本日の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}