本日のC.A.D.

Quantified Formula: QE(forall a b c d) ((a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0 and -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0 and -1*b < 0 and -1*d < 0) => (-1*a + c = 0 and -1*b + d = 0))

https://github.com/ths-rwth/smtrat/blob/JLAMP-CDCAC/benchmarks/31.smt2
そのまま実行すると

? tst12([all,all,all,all],[b,a,c,d],(f1,f2,f3,f4,f5,f6)->imp(f1*f2*f3*f4,f5*f6),"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*a + c = 0, -1*b + d = 0",7);Ans()
 *** using the sum of squares projection.
[d,4]
[c,9]
[a,24]
[b,28]
time = 3,877 ms.
111 4121(150,127) 63963(2022,4503) 643841(28592,52664) 
 *** combined adjacent 643840 cells.
1[true,true,true,true]
time = 2min, 25,341 ms.

となり，否定が false を見る方針なら

? tst12([ex,ex,ex,ex],[b,a,c,d],(f1,f2,f3,f4,f5,f6)->f1*f2*f3*f4*not(f5*f6),"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*a + c = 0, -1*b + d = 0");Ans()
 *** using Lazard's method (MPP17).
[d,4]
[c,9]
[a,24]
[b,28]
time = 1,924 ms.
55 2057(32,44) 31935(982,2225) 0(14262,26188) 
1[false]
time = 42,614 ms.

となりますが，$p\to[q\land r]$ は $[p\to q]\land[p\to r]$，更に $[p\to q]\land[[p\land q]\to r]$ と変形できるので，分割して実行すると

? tst12([all,all,all,all],[b,a,c,d],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*a + c = 0");Ans()
 *** using Lazard's method (MPP17).
[d,3]
[c,7]
[a,18]
[b,10]
time = 1,016 ms.
35 1189(118,60) 15615(574,1077) 129501(8480,10604) 
 *** combined adjacent 129500 cells.
1[true,true,true,true]
time = 22,563 ms.

? tst12([all,all,all],[b,a,d],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),strrep("a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*b + d = 0",["c"],["a"]));Ans()
 *** using Lazard's method (MPP17).
[d,4]
[a,5]
[b,4]
time = 83 ms.
11 125(20,14) 1111(44,119) 
 *** combined adjacent 1110 cells.
1[true,true,true]
time = 133 ms.

となり，否定が false を見る方針でも

? tst12([ex,ex,ex,ex],[b,a,c,d],andx,"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*a + c != 0");Ans()
 *** using Lazard's method (MPP17).
[d,3]
[c,7]
[a,18]
[b,10]
time = 999 ms.
17 591(26,14) 7174(258,524) 0(4094,3930) 
1[false]
time = 8,024 ms.

? tst12([ex,ex,ex],[b,a,d],andx,strrep("a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*b < 0, -1*d < 0, -1*b + d != 0",["c"],["a"]),7);Ans()
 *** using the sum of squares projection.
[d,4]
[a,5]
[b,4]
time = 125 ms.
5 59(6,2) 0(20,48) 
1[false]
time = 49 ms.

のように高速化できます．

ところでこの問題，入力の 2 つの等式

$\begin{eqnarray}
&& a^3 c^2+a^3 d^2-a^2 c^3-a^2 c d^2-a^2 c+a b^2 c^2+a b^2 d^2+a c^2+a d^2-b^2 c^3-b^2 c d^2-b^2 c=0,\\
&& a^2 b c^2+a^2 b d^2-a^2 c^2 d-a^2 d^3+a^2 d+b^3 c^2+b^3 d^2-b^2 c^2 d-b^2 d^3+b^2 d-b c^2-b d^2=0
\end{eqnarray}$

は，それぞれ

$\begin{eqnarray}
&& a(a^2+b^2+1)(c^2+d^2)=c(c^2+d^2+1)(a^2+b^2),\\
&& b(a^2+b^2-1)(c^2+d^2)=d(c^2+d^2-1)(a^2+b^2)
\end{eqnarray}$

と整理できるので，辺々を $(a^2+b^2)(c^2+d^2)$ で割りたくなりますが，$0< b\ \land\ 0< d$ により，それが可能であり

$\begin{eqnarray}
&& a+\frac{a}{a^2+b^2}=c+\frac{c}{c^2+d^2},\\
&& b-\frac{b}{a^2+b^2}=d-\frac{d}{c^2+d^2}
\end{eqnarray}$

そして，$s=a+bi,\ t=c+di$ とおくと

${\displaystyle s+\frac{1}{s}=t+\frac{1}{t}}$

つまり

${\displaystyle \frac{(s-t)(st-1)}{st}=\frac{1}{s}(s-t) \left( s-\frac{\bar{{t}}}{|t|^2}\right)=0}$

ここで，再び，$\mathrm{Im}{\, s}=b>0\ \land\ \mathrm{Im}{\, \bar{t}}=-d<0$ により，$s=t$ なので

$\begin{eqnarray}
\forall a\ \forall b\ \forall c\ \forall d &&[\, a(a^2+b^2+1)(c^2+d^2)=c(c^2+d^2+1)(a^2+b^2)\\
&& \land\ b(a^2+b^2-1)(c^2+d^2)=d(c^2+d^2-1)(a^2+b^2)\\
&& \land\ 0< b\ \land\ 0< d\ \to\ [\,a=c\ \land\ b=d\,]\,]
\end{eqnarray}$

を得ます．是即ち「上半平面を定義域とする Joukowsky 変換は単射である」です．

また，上記から入力の 2 つの等式の連言は $s=t\ \lor\ st=1\ \lor s=0\ \lor\ t=0$ と等価，つまり

$\begin{eqnarray}
\forall a\ \forall b\ \forall c\ \forall d &&[\,[\, a(a^2+b^2+1)(c^2+d^2)=c(c^2+d^2+1)(a^2+b^2)\\
&& \land\ b(a^2+b^2-1)(c^2+d^2)=d(c^2+d^2-1)(a^2+b^2)\,]\\
&& \leftrightarrow\ [\,[\,a=c\ \land\ b=d\,]\ \lor\ [\,ac-bd=1\ \land\ ad+bc=0\,]\\
&& \lor\ [\,a=0\ \land\ b=0\,]\ \lor\ [\,c=0\ \land\ d=0\,]\,]\,]
\end{eqnarray}$

であることも解かるので，実行してみると

? mulp=5;

 /* -> */
? tst12([ex,ex,ex,ex],[b,a,c,d],(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)->f1*f2*not(or(or(or(f3*f4,f5*f6),f7*f8),f9*f10)),"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*a + c = 0, -1*b + d = 0, a*c - b*d = 1, a*d + b*c = 0, a = 0, b = 0, c = 0, d = 0");Ans()
 *** using Lazard's method (MPP17).
[d,6]
[c,13]
[a,45]
[b,209]
time = 17,627 ms.
987 82344(314,704) 2147780(24596,93892) 0(638480,2355568) 
1[false]
time = 1h, 44min, 23,022 ms.

 /* <- */
? tst12([ex,ex,ex,ex],[b,a,c,d],(f1,f2,f3,f4,f5,f6,f7,f8,f9,f10)->not(f1*f2)*or(or(or(f3*f4,f5*f6),f7*f8),f9*f10),"a^2*c + -1*a*c^2 + -1*a*d^2 + b^2*c + -1*a^3*c^2 + -1*a^3*d^2 + a^2*c^3 + a^2*c*d^2 + -1*a*b^2*c^2 + -1*a*b^2*d^2 + b^2*c^3 + b^2*c*d^2 = 0, -1*a^2*d + -1*b^2*d + b*c^2 + b*d^2 + -1*a^2*b*c^2 + -1*a^2*b*d^2 + a^2*c^2*d + a^2*d^3 + -1*b^3*c^2 + -1*b^3*d^2 + b^2*c^2*d + b^2*d^3 = 0, -1*a + c = 0, -1*b + d = 0, a*c - b*d = 1, a*d + b*c = 0, a = 0, b = 0, c = 0, d = 0");Ans()
 *** using Lazard's method (MPP17).
[d,6]
[c,13]
[a,45]
[b,209]
time = 17,751 ms.
987 82345(314,704) 2141738(24602,93897) 0(634478,2355040) 
1[false]
time = 1h, 43min, 47,907 ms.

といった結果を得ます．