本日のC.A.D.

$\exists a\ \exists b\ \exists c\ \forall x\ \forall y\ [\ \neg[a=0 \land b=0] \land\, [\,ax+by+c=0\ \to\ dx^2+exy+fy^2=1\,]\,]$

C.W.Brown "Simple CAD Construction and its Applications"

? tst12([ex,ex,ex,all,all],[d,e,f,a,b,c,x,y],(f1,f2,f3,f4)->not(f1*f2)*imp(f3,f4),"a==0,b==0,a*x+b*y+c==0,d*x^2+e*x*y+f*y^2==1",7);Ans()
 *** using the sum of squares projection.
[y,2]
[x,4]
[c,7]
[b,15]
[a,1]
[f,27]
[e,1]
[d,1]
time = 2,808 ms.
3 9(0,0) 115(102,69) 345(0,0) 1640(2712,1450) 7840(1840,692) 47180(7340,5152) 80(1712,24) 
 *** combined adjacent 64 cells.
1[d = [d,1],e = [e,1],[f,1] < f,true,true,true,true,true]
2[[d,1] < d,e < [e,1],f = [4*f*d-e^2,1],true,true,true,true,true]
3[[d,1] < d,e = [e,1],f = [f,1],true,true,true,true,true]
4[[d,1] < d,[e,1] < e,f = [4*f*d-e^2,1],true,true,true,true,true]
time = 19,025 ms.

? tst12([ex,ex,ex,all,all],[f,d,e,a,b,c,x,y],(f1,f2,f3,f4)->not(f1*f2)*imp(f3,f4),"a==0,b==0,a*x+b*y+c==0,d*x^2+e*x*y+f*y^2==1",7);Ans()
 *** using the sum of squares projection.
[y,2]
[x,4]
[c,7]
[b,15]
[a,1]
[e,27]
[d,1]
[f,1]
time = 2,257 ms.
3 9(0,0) 115(482,107) 345(0,0) 1640(2834,1498) 7840(1832,660) 47280(7452,5092) 88(1712,24) 
 *** combined adjacent 72 cells.
1[f = [f,1],[d,1] < d,e = [e,1],true,true,true,true,true]
2[[f,1] < f,d = [d,1],e = [e,1],true,true,true,true,true]
3[[f,1] < f,[d,1] < d,e = [-4*f*d+e^2,1] or e = [-4*f*d+e^2,2],true,true,true,true,true]
time = 15,817 ms.

Wolfram Language 12.3.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= SetSystemOptions["InequalitySolvingOptions"->"CADSortVariables"->False];                                 

In[2]:= CylindricalDecomposition[Exists[{a,b,c},Not[a==0 && b==0],ForAll[{x,y},a*x+b*y+c==0,d*x^2+e*x*y+f*y^2==1]
],{d,e,f}]// Timing                                                                                              

Out[2]= {6.796608, (d == 0 && e == 0 && f > 0) || (d > 0 && f == e^2/(4*d))}

In[3]:= CylindricalDecomposition[Exists[{a,b,c},Not[a==0 && b==0],ForAll[{x,y},a*x+b*y+c==0,d*x^2+e*x*y+f*y^2==1]
],{f,d,e}]// Timing                                                                                              

Out[3]= 
{6.390617, (f == 0 && d > 0 && e == 0) || 
  (f > 0 && ((d == 0 && e == 0) || (d > 0 && (e == -2*Sqrt[d*f] || e == 2*Sqrt[d*f]))))}