? 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}
