本日のC.A.D.
? tst12([all,all],[a,b,c,x,y],(f1,f2)->imp(f1,f2),"x^8+y^8<1,a*x+b*y+c<0"); *** using Lazard's method (MPP17). [y,2] [x,4] [c,10] [b,12] [a,1] time = 14144 ms. 3 65(206,12) 963(196,62) 9219(384,432) 4385(8672,876) *** combined adjacent 4376 cells. time = 6,522 ms. ? tst12([all,all],[a,b,c,x,y],(f1,f2)->imp(f1,f2),"x^8+y^8<1,a*x+b*y+c<0",17); *** using Lazard's method (BM20). 2 [y,2] 0,0 [x,4] [c,5] [b,11] [a,1] [[[a],[],[c],[],[]],[[a],[b],[c],[],[]]] time = 15104 ms. 3 65(158,11) 615(178,21) 5439(352,392) 4385(5952,540) *** combined adjacent 4376 cells. time = 4,781 ms. ? tst12([all,all],[a,b,c,x,y],(f1,f2)->imp(f1,f2),"x^8+y^8<1,a*x+b*y+c<0",7); *** using the sum of squares projection. [y,2] [x,4] [c,10] [b,12] [a,1] time = 14724 ms. 3 65(174,12) 615(190,22) 4503(372,272) 3665(5952,540) *** combined adjacent 3656 cells. time = 4,693 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, Inc. In[1]:= CylindricalDecomposition[ForAll[{x,y},x^8+y^8<1,a*x+b*y+c<0],{a,b,c},"Function"];//Timing Out[1]= {11094.458733, Null} (* The number of the top level cells is 129. *) In[2]:= CylindricalDecomposition[ForAll[{x,y},x^8+y^8<1,a*x+b*y+c<0],{a,b,c},"Function",WorkingPrecision->30];//Timing Out[2]= {3.261566, Null}
本日のC.A.D.
? tst12([all,all,all],[a,b,c,d,x,y,z],(f1,f2)->imp(f1,f2),"x^2+y^2+z^2<1,a*x+b*y+c*z+d<0"); *** using Lazard's method (MPP17). [z,2] [y,3] [x,6] [d,11] [c,11] [b,8] [a,1] time = 284 ms. 3 33(10,8) 499(36,111) 12849(20,2411) 183385(6996,10276) 1316645(103416,51316) 126493(100772,22500) *** combined adjacent 126394 cells. time = 7min, 21,745 ms. ? tst12([all,all,all],[a,b,c,d,x,y,z],(f1,f2)->imp(f1,f2),"x^2+y^2+z^2<1,a*x+b*y+c*z+d<0",17); *** using Lazard's method (BM20). 4 [z,2] 2,2 [y,3] 0,0,0,0 [x,6] [d,5] [c,6] [b,5] [a,1] [[[a],[],[],[d],[],[],[]],[[a],[],[c],[d],[],[],[]],[[a],[b],[],[d],[],[],[]],[[a],[b],[c],[d],[],[],[]]] time = 12008 ms. 3 17(4,5) 107(14,18) 1477(14,313) 17317(1516,2164) 112289(12280,5844) 24733(11372,2236) *** combined adjacent 24718 cells. time = 16,199 ms. ? tst12([all,all,all],[a,b,c,d,x,y,z],(f1,f2)->imp(f1,f2),"x^2+y^2+z^2<1,a*x+b*y+c*z+d<0",7); *** using the sum of squares projection. [z,2] [y,3] [x,6] [d,11] [c,11] [b,8] [a,1] time = 890 ms. 3 33(10,8) 99(40,19) 1101(42,185) 9557(916,1200) 45449(14556,5636) 13677(8396,1316) *** combined adjacent 13578 cells. time = 9,539 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, Inc. In[1]:= CylindricalDecomposition[ForAll[{x,y,z},x^2+y^2+z^2<1,a*x+b*y+c*z+d<0],{a,b,c,d},"Function"];//Timing Out[1]= {0.895309, Null} In[2]:= SetSystemOptions["InequalitySolvingOptions"->{"BrownProjection" -> False, "LazardProjection" -> True}]; In[3]:= CylindricalDecomposition[ForAll[{x,y,z},x^2+y^2+z^2<1,a*x+b*y+c*z+d<0],{a,b,c,d},"Function"];//Timing Out[3]= {45.805342, Null}
本日のC.A.D.
? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); *** using Lazard's method (MPP17). [y,1] [x,3] [c,11] [b,41] [a,1] time = 414 ms. 3 217(188,41) 5631(66,259) 64685(1784,2346) 89867(26164,0) *** combined adjacent 14984 cells. time = 35,899 ms. ? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0",17); *** using Lazard's method (BM20). 1 [y,1] 0,0,0 [x,3] 0,0,0,0,0,0 [c,10] [b,35] [a,1] [[[a],[b],[],[],[]],[[a],[b],[c],[],[]]] time = 3342 ms. 3 185(159,35) 4399(66,216) 49277(1528,1962) 68427(19780,0) *** combined adjacent 11532 cells. time = 26,522 ms. ? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0",7); *** using the sum of squares projection. [y,1] [x,3] [c,11] [b,41] [a,1] time = 1010 ms. 3 217(188,41) 5247(70,217) 45213(1362,800) 54139(23860,0) *** combined adjacent 13752 cells. time = 26,332 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, Inc. In[1]:= CylindricalDecomposition[(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0,{a,b,c,x,y}];//Timing Out[1]= {190.523487, Null} (* The number of the top level cells is 35789. *)
本日のC.A.D.
Mathematica による結果の検証.
? tst12([],[a,b,c,d,e,f,x],(f1,f2,f3,f4,f5,f6,f7)->f1*f2*f3*f4*f5*f6*f7,"a==0,b<0,c<0,d==0,e<0,a*x^2+b*x+c>0,d*x^2+e*x+f<0",11);Ans(1) *** roots will be displayed in [pol,[zero,root,multi,deg]] for mma. *** using Lazard's method (MPP17). [x,2] [f,3] [e,4] [d,1] [c,3] [b,1] [a,1] time = 156 ms. 1 1(0,0) 1(0,0) 1(0,0) [[a,b,c,d],[0,-1,-1,0]]:e^2*a+(-e*d*b+d^2*c)>>(-e*b+2*d*c) [[a,b,c,d],[0,-1,-1,0]]:e^2*a+(-2*e*d*b+4*d^2*c)>>(-2*e*b+8*d*c) 1(0,3) [[a,b,c,d,e],[0,-1,-1,0,-1]]:f^2*a^2+(-f*e*b+(-2*f*d+e^2)*c)*a+(f*d*b^2-e*d*c*b+d^2*c^2)>>-2*f*c*a+(f*b^2-e*c*b+2*d*c^2) 5(0,0) 1(0,2) *** combined adjacent 0 cells. time = 87 ms. *** "Reduce"ing the conjunctions. {0.239348, Null} *** verifying the equivalence. {0.009403, True} 1[a = [a,[1,1,1,1]],b < [b,[1,1,1,1]],c < [c,[1,1,1,1]],d = [d,[1,1,1,1]],e < [e,[1,1,1,1]],f < [f*b^2-e*c*b,[1,1,1,1]],[e*x+f,[1,1,1,1]] < x < [b*x+c,[1,1,1,1]]] time = 7 ms.
本日のC.A.D.
? tst12([],[a,b,c,x],f1->f1,"a*x^2+(a+b)*x+b*c<1",17); *** using Lazard's method (BM20). -5 [x,1] 0 [c,1] [b,1] [a,1] [[[a],[b],[],[]],[[a+4],[b],[],[]]] time = 264 ms. 5 15(0,0) [[a,b],[-4,0]]:-a^2+((4*c-2)*b-4)*a-b^2>>(4*c-2)*a-2*b 33(0,0) 45(22,0) *** combined adjacent 0 cells. time = 10 ms. ? pp %2 = [[a,a+4],[b],[-a^2+((4*c-2)*b-4)*a-b^2],[a*x^2+(a+b)*x+(c*b-1)]]
QEPCAD B による結果の検証.
? qepcad3("[a x^2+(a+b) x+b c<1].","",""); *** simplifing by QEPCAD B. < gp2qe.i1 > gp2qe.o1 (with sol T) 0.05user 0.01system 0:00.07elapsed 93%CPU (0avgtext+0avgdata 8772maxresident)k 0inputs+0outputs (0major+1373minor)pagefaults 0swaps [ a = 0 /\ b^2 + 2 a b + a^2 + 4 a = 0 ] \/ [ b^2 + 2 a b + a^2 + 4 a < 0 /\ b = 0 ] \/ [ a < 0 /\ 4 a b c - b^2 - 2 a b - a^2 - 4 a > 0 ] \/ [ a < 0 /\ a x^2 + b x + a x + b c - 1 < 0 ] \/ [ 4 a b c - b^2 - 2 a b - a^2 - 4 a < 0 /\ a x^2 + b x + a x + b c - 1 < 0 ] *** simplifing by QEPCAD B. < gp2qe.i2 > gp2qe.o2 (with sol E) 0.05user 0.00system 0:00.05elapsed 89%CPU (0avgtext+0avgdata 8796maxresident)k 0inputs+0outputs (0major+1372minor)pagefaults 0swaps [ b = 0 /\ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a ] \/ [ b = 0 /\ b^2 + 2 a b + a^2 + 4 a < 0 ] \/ [ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a /\ 4 a b c - b^2 - 2 a b - a^2 - 4 a > 0 ] \/ [ b < _root_-1 b^2 + 2 a b + a^2 + 4 a /\ 4 a b c - b^2 - 2 a b - a^2 - 4 a > 0 ] \/ [ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a /\ a x^2 + b x + a x + b c - 1 < 0 ] \/ [ b < _root_-1 b^2 + 2 a b + a^2 + 4 a /\ a x^2 + b x + a x + b c - 1 < 0 ] \/ [ 4 a b c - b^2 - 2 a b - a^2 - 4 a < 0 /\ a x^2 + b x + a x + b c - 1 < 0 ] *** simplifing by QEPCAD B. < gp2qe.i3 > gp2qe.o3 (with sol N) 0.04user 0.01system 0:00.06elapsed 88%CPU (0avgtext+0avgdata 8712maxresident)k 0inputs+0outputs (0major+1372minor)pagefaults 0swaps [ b = 0 /\ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a ] \/ [ b = 0 /\ b^2 + 2 a b + a^2 + 4 a < 0 ] \/ [ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a /\ 4 a b c - b^2 - 2 a b - a^2 - 4 a > 0 ] \/ [ b < _root_-1 b^2 + 2 a b + a^2 + 4 a /\ 4 a b c - b^2 - 2 a b - a^2 - 4 a > 0 ] \/ [ b >= _root_-1 b^2 + 2 a b + a^2 + 4 a /\ a x^2 + b x + a x + b c - 1 < 0 ] \/ [ b < _root_-1 b^2 + 2 a b + a^2 + 4 a /\ a x^2 + b x + a x + b c - 1 < 0 ] \/ [ 4 a b c - b^2 - 2 a b - a^2 - 4 a < 0 /\ a x^2 + b x + a x + b c - 1 < 0 ] *** processing QEPCAD B's results. < gp2qe.i4 > gp2qe.o4 (with sol E) 0.00user 0.00system 0:00.01elapsed 93%CPU (0avgtext+0avgdata 8600maxresident)k 0inputs+0outputs (0major+1368minor)pagefaults 0swaps a x^2 + b x + a x + b c - 1 < 0 *** processing QEPCAD B's results. < gp2qe.i5 > gp2qe.o5 (with sol N) 0.00user 0.00system 0:00.02elapsed 75%CPU (0avgtext+0avgdata 8596maxresident)k 0inputs+0outputs (0major+1369minor)pagefaults 0swaps a x^2 + b x + a x + b c - 1 < 0 *** verifying the equivalence. < gp2qe.e6 (with sol E) TRUE 0.01user 0.00system 0:00.02elapsed 72%CPU (0avgtext+0avgdata 8672maxresident)k 0inputs+0outputs (0major+1372minor)pagefaults 0swaps *** verifying the equivalence. < gp2qe.e7 (with sol N) TRUE 0.01user 0.00system 0:00.03elapsed 53%CPU (0avgtext+0avgdata 8828maxresident)k 0inputs+0outputs (0major+1370minor)pagefaults 0swaps time = 5 ms.
本日のC.A.D.
? tst12([],[a,b,c,x,y],(f1,f2)->f1*f2,"y>=0,y+(a-b)*x^2+(2*a-3*b+c)*a*x+c-b<=0");pp *** using Lazard's method (MPP17). [y,2] [x,1] [c,2] [b,2] [a,4] time = 134 ms. 11 57(6,2) 315(36,26) 1219(148,0) 1592(0,946) *** combined adjacent 786 cells. time = 415 ms. %1 = [[a,2*a^2-1,3*a-2,3*a+2],[a-b,4*a^4-12*b*a^3+9*b^2*a^2+4*b*a-4*b^2],[b-c,4*a^4+(-12*b+4*c)*a^3+(9*b^2-6*c*b+c^2)*a^2+(4*b-4*c)*a+(-4*b^2+4*c*b)],[(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(-b+c)],[y,(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(y+(-b+c))]] ? tst12([],[a,b,c,x,y],(f1,f2)->f1*f2,"y>=0,y+(a-b)*x^2+(2*a-3*b+c)*a*x+c-b<=0",17);pp *** using Lazard's method (BM20). [y,2] 1 [x,1] 0 [c,2] [b,1] [a,2] [[[a],[b],[],[],[]]] time = 680 ms. 7 21(0,0) 87(20,18) 335(28,0) 434(0,274) *** combined adjacent 214 cells. time = 118 ms. %2 = [[a,2*a^2-1],[a-b],[4*a^4+(-12*b+4*c)*a^3+(9*b^2-6*c*b+c^2)*a^2+(4*b-4*c)*a+(-4*b^2+4*c*b),b-c],[(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(-b+c)],[(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(y+(-b+c)),y]] ? tst12([],[a,b,c,x,y],(f1,f2)->f1*f2,"y>=0,y+(a-b)*x^2+(2*a-3*b+c)*a*x+c-b<=0",7);pp *** using the sum of squares projection. [y,2] [x,1] [c,2] [b,2] [a,4] time = 163 ms. 7 21(2,2) 63(34,14) 215(28,0) 278(0,178) *** combined adjacent 142 cells. time = 85 ms. %3 = [[a,2*a^2-1,5*a^2-6*a+2,5*a^2+6*a+2],[a-b,16*a^8-96*b*a^7+(216*b^2+4)*a^6+(-216*b^3+32*b)*a^5+(81*b^4-128*b^2-8)*a^4+(168*b^3+8*b)*a^3+(-72*b^4+16*b^2+5)*a^2+(-32*b^3-8*b)*a+(16*b^4+4*b^2)],[10*a^4+(-38*b+8*c)*a^3+(53*b^2-20*c*b+2*c^2)*a^2+(-34*b^3+16*c*b^2-2*c^2*b)*a+(10*b^4-6*c*b^3+(c^2+1)*b^2-2*c*b+c^2),4*a^4+(-12*b+4*c)*a^3+(9*b^2-6*c*b+c^2)*a^2+(4*b-4*c)*a+(-4*b^2+4*c*b)],[(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(-b+c)],[y,(a-b)*x^2+(2*a^2+(-3*b+c)*a)*x+(y+(-b+c))]]
C.W.Brown, S.McCallum "Enhancements to Lazard’s Method for Cylindrical Algebraic Decomposition"
本日のC.A.D.
? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); [y,1] [x,3] [c,11] [b,41] [a,1] time = 635 ms. 3 217(188,41) 5631(66,259) 64685(1784,2346) 89877(26166,0) *** combined adjacent 14994 cells. time = 36,295 ms. ? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); *** using the modified Lazard's projection. [y,1] [x,3] [c,10] [b,35] [a,1] [[a,b,c],[a,b,c],[a,b,c],[a,b],[a,b],[a,b],[a,b],[a,b],[a,b]] time = 3532 ms. 3 185(159,35) 4399(66,216) 49277(1528,1962) 68437(19782,0) *** combined adjacent 11542 cells. time = 28,779 ms. ? tst12([],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0",7); *** using the sum of squares projection. [y,1] [x,3] [c,11] [b,41] [a,1] time = 1000 ms. 3 217(188,41) 5247(70,217) 45213(1362,800) 54149(23862,0) *** combined adjacent 13762 cells. time = 28,612 ms.
? tst12([ex,ex],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); [y,1] [x,3] [c,11] [b,41] [a,1] time = 414 ms. 3 217(188,41) 5631(66,259) 64683(1784,2346) 5631(3936,0) *** combined adjacent 5630 cells. time = 8,926 ms. ? tst12([ex,ex],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0"); *** using the modified Lazard's projection. [y,1] [x,3] [c,10] [b,35] [a,1] [[a,b,c],[a,b,c],[a,b,c],[a,b],[a,b],[a,b],[a,b],[a,b],[a,b]] time = 3440 ms. 3 185(159,35) 4399(66,216) 49275(1528,1962) 4399(2928,0) *** combined adjacent 4398 cells. time = 7,138 ms. ? tst12([ex,ex],[a,b,c,x,y],f->f,"(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0",7); *** using the sum of squares projection. [y,1] [x,3] [c,11] [b,41] [a,1] time = 979 ms. 3 217(188,41) 5247(70,217) 45211(1362,800) 5247(3680,0) *** combined adjacent 5246 cells. time = 12,066 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit) Copyright 1988-2021 Wolfram Research, Inc. In[1]:= SetSystemOptions["InequalitySolvingOptions"->{"BrownProjection" -> False, "LazardProjection" -> True}]; In[2]:= CylindricalDecomposition[(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0,{a,b,c,x,y}];//Timing Out[2]= {181.187008, Null} In[3]:= CylindricalDecomposition[Exists[{x,y},(a*x^2+b*x-c)*y^2+(b*x^2+c*x-a)*y+c*x^2+a*x-b==0],{a,b,c}]//Timing Out[3]= {2.216417, True}