本日のC.A.D.

Kahan’s ellipse problem (SIGSAM Bulletin, 9, 11, 1975)

楕円周が単位開円板に含まれるための条件

a^2＞0 ∧ b^2＞0 ∧ ∀x∀y({(x-c)^2}/{a^2}+{(y-d)^2}/{b^2}＝1 → x^2+y^2＜1)
を a^2，b^2，c^2，d^2 についての多項式による不等式の連言で表すには少なくとも何個の不等式が必要か？

は C.A.D. による QE が困難な例です．

C.W.Brown "Improved Projection for Cylindrical Algebraic Decomposition"
N.I.Ioakimidis "Kahan’s ellipse problem, quantifier elimination and computational mechanics"

今回はこれを equational constraint に対する McCallum の結果と Lazard method (2020) を用いて QE します．

まず，冒頭の論理式を F(a，b，c，d) とし，x，y をそれぞれ ±x，±y（複号任意）に置き換えると，F(a，b，c，d) は F(a，b，±c，±d) と等価であることが判るので

c≧0 ∧ d≧0 ∧ F(a，b，-c，-d)
を G(a，b，c，d) とすると，F(a，b，c，d) はG(a，b，-c，-d) ∨ G(a，b，-c，d) ∨ G(a，b，c，-d) ∨ G(a，b，c，d)
のように G を用いて表せます．そして，x，y をそれぞれ y，x に置き換えると，G(a，b，c，d) は G(b，a，d，c) と等価であることが判るのでa^2≧b^2 ∧ G(a，b，c，d)
を H(a，b，c，d) とすると，G(a，b，c，d) はH(a，b，c，d) ∨ H(b，a，d，c)
のように H を用いて表せます．さらに，x，y をそれぞれ x-c，y-d に置き換えると，H(a，b，c，d) は{b^2}/{a^2}≦1 ∧ b^2＞0 ∧ c≧0 ∧ d≧0 ∧ ∀x∀y({b^2 x^2}/{a^2}+y^2＝b^2 → (x-c)^2+(y-d)^2＜1)
のように表せるのでa＞0 ∧ a≦1 ∧ b＞0 ∧ c≧0 ∧ d≧0 ∧ ∀x∀y(a x^2+y^2＝b → (x-c)^2+(y-d)^2＜1)
を I(a，b，c，d) とすると，H(a，b，c，d) は I({b^2}/{a^2}，b^2，c，d) と表せます．最後に，I の量化されている部分式，それより左の部分式をそれぞれ Q，P とするとI ＝ P ∧ Q ＝ P ∧ ((￢P) ∨ Q) ＝ P ∧ ￢(P ∧ ￢Q)
となるので，P ∧ ￢Q，つまり，∃x∃y(a＞0 ∧ a≦1 ∧ b＞0 ∧ c≧0 ∧ d≧0 ∧ a x^2+y^2＝b ∧ (x-c)^2+(y-d)^2≧1)
を QE すればよいことが判ります．

? AL=projs3([d,c,a,b,x],[a-1,a,b,c,d,a*x^2-b,polresultant((x-c)^2+(y-d)^2-1,a*x^2+y^2-b,y)]);
 *** using Lazard's method (BM20) with realrad.
0,0
[x,2]
0
[b,3]
-6,0,-6
[a,5]
-6,-6,-6,-6,-6,-6
[c,14]
[d,27]
time = 7,516 ms.

? tst12([ex,ex],[d,c,a,b,x,y],andx,"0<a,a<=1,0<b,0<=c,0<=d,(x-c)^2+(y-d)^2>=1,a*x^2+y^2==b",17,concat(AL[3],[[(x-c)^2+(y-d)^2-1,a*x^2+y^2-b]]));
60 794(140,84) 3800(1296,599) 35573(1742,2460) 281351(20934,12042) 34061(74736,10384) 
 *** combined adjacent 33767 cells.
time = 1min, 46,775 ms.