MomentTools

   _       _ _(_)_     |  Documentation: https://docs.julialang.org
  (_)     | (_) (_)    |
   _ _   _| |_  __ _   |  Type "?" for help, "]?" for Pkg help.
  | | | | | | |/ _` |  |
  | | |_| | | | (_| |  |  Version 1.6.0 (2021-03-24)
 _/ |\__'_|_|_|\__'_|  |  Official https://julialang.org/ release
|__/                   |

julia> using DynamicPolynomials, MultivariateSeries, MomentTools, CSDP; optimizer = CSDP.Optimizer;

julia> X=@polyvar x y z; f = (x - y + z)^2 + (x*y + z)^2*z^2;

julia> @time M=minimize(f,[f],[],X,8,optimizer)[2];
CSDP 6.2.0
Iter:  0 Ap: 0.00e+00 Pobj:  0.0000000e+00 Ad: 0.00e+00 Dobj:  0.0000000e+00 
Iter:  1 Ap: 5.70e-01 Pobj: -2.8807304e+01 Ad: 3.84e-01 Dobj:  3.5564608e+00 
Iter:  2 Ap: 6.69e-01 Pobj: -1.6858129e+02 Ad: 5.68e-01 Dobj: -6.3657488e-01 
Iter:  3 Ap: 7.00e-01 Pobj: -2.0815594e+02 Ad: 7.78e-01 Dobj:  6.9461464e-02 
Iter:  4 Ap: 6.24e-01 Pobj: -1.8003880e+02 Ad: 7.44e-01 Dobj:  1.9621905e-02 
Iter:  5 Ap: 7.44e-01 Pobj: -8.9451385e+01 Ad: 6.98e-01 Dobj:  7.6521211e-03 
Iter:  6 Ap: 5.50e-01 Pobj: -5.6777715e+01 Ad: 6.27e-01 Dobj:  3.0835452e-03 
Iter:  7 Ap: 4.99e-01 Pobj: -3.8357170e+01 Ad: 6.95e-01 Dobj:  1.1243439e-03 
Iter:  8 Ap: 3.32e-01 Pobj: -2.8849786e+01 Ad: 5.75e-01 Dobj:  5.2802817e-04 
Iter:  9 Ap: 6.12e-01 Pobj: -1.3830209e+01 Ad: 5.50e-01 Dobj:  2.6789401e-04 
Iter: 10 Ap: 4.52e-01 Pobj: -8.9989526e+00 Ad: 5.26e-01 Dobj:  1.2846141e-04 
Iter: 11 Ap: 3.90e-01 Pobj: -6.3929357e+00 Ad: 6.63e-01 Dobj:  4.1832560e-05 
Iter: 12 Ap: 3.32e-01 Pobj: -4.6413747e+00 Ad: 4.69e-01 Dobj:  2.3404997e-05 
Iter: 13 Ap: 4.76e-01 Pobj: -2.7582583e+00 Ad: 5.44e-01 Dobj:  1.1072798e-05 
Iter: 14 Ap: 4.10e-01 Pobj: -1.8170471e+00 Ad: 6.20e-01 Dobj:  4.1075038e-06 
Iter: 15 Ap: 4.88e-01 Pobj: -1.0510459e+00 Ad: 6.41e-01 Dobj:  1.4327908e-06 
Iter: 16 Ap: 4.02e-01 Pobj: -6.8407656e-01 Ad: 5.13e-01 Dobj:  6.8574504e-07 
Iter: 17 Ap: 2.75e-01 Pobj: -5.2423749e-01 Ad: 6.05e-01 Dobj:  2.5673497e-07 
Iter: 18 Ap: 4.76e-01 Pobj: -2.9920946e-01 Ad: 5.53e-01 Dobj:  1.2237666e-07 
Iter: 19 Ap: 4.07e-01 Pobj: -1.9097099e-01 Ad: 5.77e-01 Dobj:  5.9944913e-08 
Iter: 20 Ap: 4.69e-01 Pobj: -1.1328837e-01 Ad: 7.34e-01 Dobj:  2.6270395e-08 
Iter: 21 Ap: 6.91e-01 Pobj: -4.0718196e-02 Ad: 9.91e-01 Dobj:  1.4905678e-08 
Iter: 22 Ap: 7.98e-01 Pobj: -8.8267883e-03 Ad: 1.00e+00 Dobj:  1.4712661e-08 
Iter: 23 Ap: 9.30e-01 Pobj: -7.2753194e-04 Ad: 1.00e+00 Dobj:  1.4635985e-08 
Iter: 24 Ap: 9.52e-01 Pobj: -4.6444681e-05 Ad: 1.00e+00 Dobj:  1.4511251e-08 
Iter: 25 Ap: 9.77e-01 Pobj: -2.3128726e-06 Ad: 1.00e+00 Dobj:  1.3699810e-08 
Iter: 26 Ap: 1.00e+00 Pobj: -2.9295805e-07 Ad: 1.00e+00 Dobj:  2.6620661e-09 
Iter: 27 Ap: 1.00e+00 Pobj: -1.4503259e-07 Ad: 7.98e-01 Dobj: -4.9856960e-08 
Iter: 28 Ap: 9.79e-01 Pobj: -1.3349889e-08 Ad: 1.00e+00 Dobj: -5.0993826e-08 
Iter: 29 Ap: 1.00e+00 Pobj: -6.0340429e-09 Ad: 8.18e-01 Dobj: -9.8402342e-09 
Iter: 30 Ap: 3.72e-01 Pobj: -4.7992492e-09 Ad: 5.02e-01 Dobj: -4.9055902e-09 
Iter: 31 Ap: 9.01e-01 Pobj: -1.4789741e-09 Ad: 7.05e-01 Dobj: -1.4754469e-09 
Iter: 32 Ap: 8.59e-01 Pobj: -7.0878722e-10 Ad: 7.12e-01 Dobj: -4.1004977e-10 
Iter: 33 Ap: 8.64e-01 Pobj: -3.0782665e-10 Ad: 7.84e-01 Dobj: -7.7378548e-11 
Iter: 34 Ap: 5.05e-01 Pobj: -1.9417526e-10 Ad: 6.39e-01 Dobj: -2.3950619e-11 
Success: SDP solved
Primal objective value: -1.9417526e-10 
Dual objective value: -2.3950619e-11 
Relative primal infeasibility: 9.94e-11 
Relative dual infeasibility: 5.08e-10 
Real Relative Gap: 1.70e-10 
XZ Relative Gap: 6.09e-09 
DIMACS error measures: 1.85e-10 0.00e+00 9.45e-09 0.00e+00 1.70e-10 6.09e-09
 60.145666 seconds (1.00 M allocations: 1.462 GiB, 0.08% gc time)

julia> annihilator(get_series(M)[1],monomials(X,seq(0:3)))[1]
2-element Vector{Any}:
 -0.9999999618699011z - 0.9999999886637668x + y + 2.552293999411037e-9
 -3.7243455708324547e-7z³ + 0.9999999882834394z²x + zx² + 0.9999994193028456z² + 3.24561595377304e-8zx + 4.157295047590385e-8x² - 2.6718977824777973e-7z + 6.5951240996176e-11x - 5.6543031689507833e-8

julia> X=@polyvar a x y z; f = -10*z^4 + x^3 - 3*x^2*z + 3*x*z^2 + 20*y*z^2 - z^3 - 10*x^2 + 20*x*z - 10*y^2 - 10*z^2;  g = 3*a - (x^2 + y^2 + z^2); h = y - a;

julia> @time M=minimize(f,[f,g,h],[],X,6,optimizer)[2];
CSDP 6.2.0
Iter:  0 Ap: 0.00e+00 Pobj:  0.0000000e+00 Ad: 0.00e+00 Dobj:  0.0000000e+00 
Iter:  1 Ap: 5.96e-01 Pobj: -1.1005207e+02 Ad: 2.76e-01 Dobj: -7.7938223e+00 
Iter:  2 Ap: 7.51e-01 Pobj: -9.1085191e+02 Ad: 5.65e-01 Dobj: -2.2979271e-01 
Iter:  3 Ap: 7.38e-01 Pobj: -7.3384276e+02 Ad: 8.16e-01 Dobj: -4.4983724e-02 
Iter:  4 Ap: 9.15e-01 Pobj: -5.2094408e+02 Ad: 8.58e-01 Dobj: -1.3200751e-02 
Iter:  5 Ap: 8.58e-01 Pobj: -1.1582448e+02 Ad: 8.61e-01 Dobj: -3.1098072e-03 
Iter:  6 Ap: 7.84e-01 Pobj: -1.6209634e+01 Ad: 8.62e-01 Dobj: -7.3452353e-04 
Iter:  7 Ap: 8.67e-01 Pobj: -1.6067709e+00 Ad: 7.97e-01 Dobj: -2.0667674e-04 
Iter:  8 Ap: 9.37e-01 Pobj: -1.7693850e-01 Ad: 8.96e-01 Dobj: -1.4946856e-05 
Iter:  9 Ap: 9.59e-01 Pobj: -2.3387913e-02 Ad: 9.02e-01 Dobj: -9.8436481e-07 
Iter: 10 Ap: 9.64e-01 Pobj: -3.6200040e-03 Ad: 8.17e-01 Dobj: -1.5670489e-07 
Iter: 11 Ap: 1.00e+00 Pobj: -1.0970131e-03 Ad: 8.11e-01 Dobj: -3.8383125e-08 
Iter: 12 Ap: 8.04e-01 Pobj: -1.8961449e-04 Ad: 9.26e-01 Dobj: -8.2434930e-09 
Iter: 13 Ap: 1.00e+00 Pobj: -4.4730362e-05 Ad: 1.00e+00 Dobj: -1.6209079e-10 
Iter: 14 Ap: 9.85e-01 Pobj: -1.8338375e-06 Ad: 1.00e+00 Dobj: -2.3743585e-10 
Iter: 15 Ap: 1.00e+00 Pobj: -8.6203045e-08 Ad: 1.00e+00 Dobj: -7.8350304e-10 
Iter: 16 Ap: 1.00e+00 Pobj: -1.8546492e-08 Ad: 1.00e+00 Dobj: -9.0815888e-09 
Iter: 17 Ap: 1.00e+00 Pobj: -4.3556816e-09 Ad: 1.00e+00 Dobj: -1.7330145e-08 
Iter: 18 Ap: 1.00e+00 Pobj: -2.8109923e-10 Ad: 1.00e+00 Dobj: -1.8244192e-08 
Iter: 19 Ap: 9.85e-01 Pobj: -3.8411063e-11 Ad: 8.90e-01 Dobj: -2.3176021e-09 
Iter: 20 Ap: 1.00e+00 Pobj: -1.5746583e-11 Ad: 8.21e-01 Dobj: -4.2504311e-10 
Iter: 21 Ap: 3.71e-01 Pobj: -9.2716806e-13 Ad: 7.83e-01 Dobj: -9.1993080e-11 
Success: SDP solved
Primal objective value: -9.2716806e-13 
Dual objective value: -9.1993080e-11 
Relative primal infeasibility: 7.92e-09 
Relative dual infeasibility: 3.07e-09 
Real Relative Gap: -9.11e-11 
XZ Relative Gap: 6.84e-09 
DIMACS error measures: 1.36e-08 0.00e+00 1.95e-07 0.00e+00 -9.11e-11 6.84e-09
 33.597916 seconds (2.16 M allocations: 3.818 GiB, 0.47% gc time)

julia> annihilator(get_series(M)[1],monomials(X,seq(0:3)))[1]
5-element Vector{Any}:
 -1.0000000000102727a - 2.1609837237432704e-13x + y + 3.4714428691621264e-12
 -1.6534928112712892e-7a - 1.000001169818265x + z + 2.916073255320562e-8
 a² - 1.0000076240241975a - 5.130771092653218e-7x + 2.3525318446283505e-6
 ax + 1.0707232983808452e-5a - 0.9999983573879418x - 1.12304474871292e-5
 x² - 0.9999950150761634a + 3.9272360301160237e-7x - 1.1773485627254423e-6

julia> X=@polyvar x y; f = (x^2-2)^2+(x-y^2)^2;

julia> @time M=minimize(f,[f],[],X,8,optimizer)[2];
CSDP 6.2.0
Iter:  0 Ap: 0.00e+00 Pobj:  0.0000000e+00 Ad: 0.00e+00 Dobj:  0.0000000e+00 
Iter:  1 Ap: 8.30e-01 Pobj: -6.4429837e+00 Ad: 5.84e-01 Dobj:  2.1188634e+00 
Iter:  2 Ap: 8.86e-01 Pobj:  8.6485244e+00 Ad: 7.52e-01 Dobj: -1.0092169e-01 
Iter:  3 Ap: 5.73e-01 Pobj:  6.3082468e+02 Ad: 2.85e-01 Dobj:  6.7429840e-01 
Iter:  4 Ap: 1.18e-01 Pobj:  1.0196791e+03 Ad: 4.55e-01 Dobj:  2.6642941e-01 
Iter:  5 Ap: 7.26e-01 Pobj:  2.0191291e+01 Ad: 4.66e-01 Dobj:  5.9874760e-02 
Iter:  6 Ap: 7.75e-01 Pobj:  3.9340988e+01 Ad: 7.50e-01 Dobj: -2.3326518e-03 
Iter:  7 Ap: 5.60e-01 Pobj:  2.7275880e+01 Ad: 8.59e-01 Dobj:  5.1133315e-03 
Iter:  8 Ap: 9.32e-01 Pobj:  1.6027470e+00 Ad: 8.66e-01 Dobj: -2.6751064e-04 
Iter:  9 Ap: 9.47e-01 Pobj:  7.4490606e-02 Ad: 9.23e-01 Dobj:  1.5463716e-05 
Iter: 10 Ap: 9.54e-01 Pobj:  2.4705712e-03 Ad: 9.44e-01 Dobj:  3.1920954e-07 
Iter: 11 Ap: 9.62e-01 Pobj:  3.1228085e-05 Ad: 9.70e-01 Dobj:  3.3330596e-08 
Iter: 12 Ap: 1.00e+00 Pobj: -2.3272240e-05 Ad: 1.00e+00 Dobj:  1.0627952e-08 
Iter: 13 Ap: 9.91e-01 Pobj: -1.2872806e-06 Ad: 1.00e+00 Dobj:  9.8126343e-09 
Iter: 14 Ap: 1.00e+00 Pobj: -1.4435182e-07 Ad: 1.00e+00 Dobj: -3.6250984e-09 
Iter: 15 Ap: 1.00e+00 Pobj:  5.5437355e-08 Ad: 9.48e-01 Dobj: -8.9896287e-08 
Iter: 16 Ap: 1.00e+00 Pobj:  5.9516053e-08 Ad: 1.00e+00 Dobj: -4.4506443e-08 
Iter: 17 Ap: 1.00e+00 Pobj:  1.5428438e-08 Ad: 1.00e+00 Dobj: -5.5963527e-09 
Iter: 18 Ap: 1.00e+00 Pobj:  2.4170027e-08 Ad: 9.98e-01 Dobj: -2.1061730e-10 
Success: SDP solved
Primal objective value: 2.4170027e-08 
Dual objective value: -2.1061730e-10 
Relative primal infeasibility: 9.65e-12 
Relative dual infeasibility: 1.69e-09 
Real Relative Gap: -2.44e-08 
XZ Relative Gap: 8.13e-09 
DIMACS error measures: 1.27e-11 0.00e+00 1.85e-08 0.00e+00 -2.44e-08 8.13e-09
  5.170052 seconds (97.46 k allocations: 14.575 MiB, 0.26% gc time)

julia> annihilator(get_series(M)[1],monomials(X,seq(0:3)))[1]
2-element Vector{Any}:
 x - 1.4142135219640146
 y² - 1.41421349394504

https://arxiv.org/pdf/2102.09367.pdf
https://gitlab.inria.fr/AlgebraicGeometricModeling/MomentTools.jl

本日のC.A.D.

? tst12([all,all],[b,a,c,x,y],(f1,f2,f3,f4)->f1*f2*imp(f3,f4),"0<a,0<b,a*(x-c)^2+b*(y-1)^2<1,x^2+y^2<2",17);
 *** using Lazard's method (BM20) with realrad.
2
[y,2]
-6,-6,0
[x,4]
0,-6,-6,-6,0,0
[c,6]
-6,-6,-6,-6,-6,-6
[a,19]
[b,88]
time = 2,760 ms.
195 7267(66,222) 204071(1928,8123) 2944009(51650,175582) 74736(665464,86944) 
 *** combined adjacent 74625 cells.
time = 40min, 40,702 ms.

? tst12([all,all],[b,a,c,x,y],(f1,f2,f3,f4)->f1*f2*imp(f3,f4),"0<a,0<b,a*(x-c)^2+b*(y-1)^2<1,x^2+y^2<2",7);
 *** using the sum of squares projection.
[y,2]
[x,4]
[c,7]
[a,24]
[b,133]
time = 5,272 ms.
141 5383(44,156) 161955(1406,6706) 1919543(38100,124228) 16266(512878,62332) 
 *** combined adjacent 16221 cells.
time = 21min, 12,041 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[0<a&&0<b&&ForAll[{x,y},a*(x-c)^2+b*(y-1)^2<1,x^2+y^2<2],{b,a,c},"Function"]
;//Timing                                                                                                       

Out[1]= {1039.502639, Null}  (* The number of the top level cells is 1618. *)

Lazard's method(その2)

2017年に続いて,2020年に発表された Brown と McCallum の論文 "Enhancements to Lazard’s Method for Cylindrical Algebraic Decomposition" https://rdcu.be/ciEY8 の主結果は次の通りです.

Lazard method の projection set に trailing coefficient を含めるのは,全ての係数が 0 となる実数の組が無限にある場合のみでよく,有限個の場合は,空でないなら,それら全てを sample point として lifting phase において順次追加し,空なら,何もしなくてよい.

このブログで最近公開している CAD のうち (BM20) の表示があるものは,この結果を採用した実装による出力であり,上記の実数の組の集合が空でない場合に,それらを特定する方法,つまり,整数係数の多変数多項式系の実数の零点集合の有限性の判定法,更に(空でない)有限の場合にそれらを零点にもつ性質の良い多項式系を求める処理を含んでいます.

具体的には「Singular の realrad 関数を用いたもの」と「CAD自体を再帰的に呼び出すもの」の 2 つを実装しており,positive/zero-dimensional 多項式系の実数の零点を統合して扱う目的からすれば前者で十分なのですが,realrad の作動は速いとは云えず,時に帰ってきません.後者は過剰性能であり,またファイルによるデータの授受を繰り返すことから問題を選びます.

Videos

Scott McCallum
http://www.casc-conference.org/2020/videos/1/01-BrownMcCallum.mp4

Chris Brown, Hoon Hong, James Davenport
https://vimeo.com/showcase/5271198
http://www.sc-square.org/CSA/school/lectures.html

Adam Strzebonski
https://youtu.be/z-3epLLUhGQ
https://youtu.be/J_iCJwtOPpA

James Davenport
https://youtu.be/oIsmANTQsxA

Marie-Francoise Roy
https://youtu.be/Ka2b666jhm8

Saugata Basu
https://youtu.be/UoHggvi8Ae8
https://youtu.be/O_idjsn3Nz4

Andre Platzer
https://youtu.be/dvm4jFhj0R4
https://youtu.be/EjiqDs26Ce4

Mohab Safey El Din
https://youtu.be/ZPt_Hsy21OI

本日のC.A.D.

? tst12([all,all,all],[a,b,c,d,e,f,x,y,z],id,"((a*x+b)*y+c)*z+((d*x+e)*y+f)<0");Ans()
 *** using Lazard's method (MPP17).
[z,1]
[y,2]
[x,3]
[f,3]
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
time = 74 ms.
3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1257(0,396) 5800(0,1204) 23424(0,1720) 1(0,0) 
 *** combined adjacent 0 cells.
1[a = [a,1],b = [b,1],c = [c,1],d = [d,1],e = [e,1],f < [f,1],true,true,true]
time = 1,867 ms.

/*  realrad version */

? tst12([all,all,all],[a,b,c,d,e,f,x,y,z],id,"((a*x+b)*y+c)*z+((d*x+e)*y+f)<0",17);Ans()
 *** using Lazard's method (BM20).
6
[z,1]
2,2
[y,2]
0,5,0
[x,3]
1,1
[f,3]
1
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
time = 37,343 ms.
[[[],[],[],[d],[e],[],[],[],[]],[[a],[b],[],[],[],[],[],[],[]]]
3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1257(0,396) 5800(0,1204) 23424(0,1720) 1(0,0) 
 *** combined adjacent 0 cells.
1[a = [a,1],b = [b,1],c = [c,1],d = [d,1],e = [e,1],f < [f,1],true,true,true]
time = 1,882 ms.

/* recursive version */

? tst12([all,all,all],[a,b,c,d,e,f,x,y,z],id,"((a*x+b)*y+c)*z+((d*x+e)*y+f)<0",19);Ans()
 1>> using Lazard's method (BM20).
[a, b, c, d, e, f, x, y],[d*y*x + (e*y + f), a*y*x + (b*y + c)]
 2>> using Lazard's method (BM20).
[a, b, c, d, e, f, x],[f, d*x + e]
 3>> using Lazard's method (BM20).
[a, b, c, d, e, f],[e, d]
 4>> using Lazard's method (BM20).
[f]
[e,1]
[d,1]
[c]
[b]
[a]
 <<4
time = 35 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0
[x,1]
[f,1]
[e]
[d,1]
[c]
[b]
[a]
 <<3
time = 111 ms.
1 1(0,0) 1(0,0) 3(0,0) 5(2,0) 5(0,0) 3(0,0) 
 *** combined adjacent 0 cells.
[a, b, c, d, e, f, x],[c, a*x + b]
 3>> using Lazard's method (BM20).
[a, b, c, d, e, f],[b, a]
 4>> using Lazard's method (BM20).
[f]
[e]
[d]
[c]
[b,1]
[a,1]
 <<4
time = 34 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0
[x,1]
[f]
[e]
[d]
[c,1]
[b]
[a,1]
 <<3
time = 109 ms.
3 5(2,0) 5(0,0) 5(0,0) 5(0,0) 5(0,0) 3(0,0) 
 *** combined adjacent 0 cells.
1,1
[y,2]
[a, b, c, d, e, f],[e, d]
 3>> using Lazard's method (BM20).
[f]
[e,1]
[d,1]
[c]
[b]
[a]
 <<3
time = 37 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
[a, b, c, d, e, f],[-f*b + e*c, -f*a + d*c, -f*e*a + f*d*b]
 3>> using Lazard's method (BM20).
[a, b, c, d, e],[b, e*c]
 4>> using Lazard's method (BM20).
[e,1]
[d]
[c,1]
[b,1]
[a]
 <<4
time = 46 ms.
1 1(0,0) 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
[a, b, c, d, e],[a, d*c]
 4>> using Lazard's method (BM20).
[e]
[d,1]
[c,1]
[b]
[a,1]
 <<4
time = 37 ms.
1 1(0,0) 3(0,0) 5(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1,1
[f,3]
[a, b, c, d],[a, d*b]
 4>> using Lazard's method (BM20).
[d,1]
[c]
[b,1]
[a,1]
 <<4
time = 42 ms.
1 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
 <<3
time = 326 ms.
3 9(0,0) 27(0,0) 69(0,0) 227(0,60) 169(0,364) 
 *** combined adjacent 142 cells.
[a, b, c, d, e, f],[b, a]
 3>> using Lazard's method (BM20).
[f]
[e]
[d]
[c]
[b,1]
[a,1]
 <<3
time = 33 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0,1,0
[x,3]
[a, b, c, d, e],[b, e*c]
 3>> using Lazard's method (BM20).
[e,1]
[d]
[c,1]
[b,1]
[a]
 <<3
time = 36 ms.
1 1(0,0) 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
[a, b, c, d, e],[a, d*c]
 3>> using Lazard's method (BM20).
[e]
[d,1]
[c,1]
[b]
[a,1]
 <<3
time = 33 ms.
1 1(0,0) 3(0,0) 5(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1,1
[f,3]
[a, b, c, d],[a, d*b]
 3>> using Lazard's method (BM20).
[d,1]
[c]
[b,1]
[a,1]
 <<3
time = 34 ms.
1 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
 <<2
time = 1,238 ms.
3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1257(0,396) 5801(0,1204) 1169(0,1496) 
 *** combined adjacent 476 cells.
1
[z,1]
[a, b, c, d, e, f, x],[f, d*x + e]
 2>> using Lazard's method (BM20).
[a, b, c, d, e, f],[e, d]
 3>> using Lazard's method (BM20).
[f]
[e,1]
[d,1]
[c]
[b]
[a]
 <<3
time = 37 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0
[x,1]
[f,1]
[e]
[d,1]
[c]
[b]
[a]
 <<2
time = 120 ms.
1 1(0,0) 1(0,0) 3(0,0) 5(2,0) 5(0,0) 3(0,0) 
 *** combined adjacent 0 cells.
[a, b, c, d, e, f, x],[c, a*x + b]
 2>> using Lazard's method (BM20).
[a, b, c, d, e, f],[b, a]
 3>> using Lazard's method (BM20).
[f]
[e]
[d]
[c]
[b,1]
[a,1]
 <<3
time = 30 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0
[x,1]
[f]
[e]
[d]
[c,1]
[b]
[a,1]
 <<2
time = 113 ms.
3 5(2,0) 5(0,0) 5(0,0) 5(0,0) 5(0,0) 3(0,0) 
 *** combined adjacent 0 cells.
1,1
[y,2]
[a, b, c, d, e, f],[e, d]
 2>> using Lazard's method (BM20).
[f]
[e,1]
[d,1]
[c]
[b]
[a]
 <<2
time = 29 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
[a, b, c, d, e, f],[-f*b + e*c, -f*a + d*c, -f*e*a + f*d*b]
 2>> using Lazard's method (BM20).
[a, b, c, d, e],[b, e*c]
 3>> using Lazard's method (BM20).
[e,1]
[d]
[c,1]
[b,1]
[a]
 <<3
time = 34 ms.
1 1(0,0) 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
[a, b, c, d, e],[a, d*c]
 3>> using Lazard's method (BM20).
[e]
[d,1]
[c,1]
[b]
[a,1]
 <<3
time = 40 ms.
1 1(0,0) 3(0,0) 5(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1,1
[f,3]
[a, b, c, d],[a, d*b]
 3>> using Lazard's method (BM20).
[d,1]
[c]
[b,1]
[a,1]
 <<3
time = 35 ms.
1 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
 <<2
time = 312 ms.
3 9(0,0) 27(0,0) 69(0,0) 227(0,60) 169(0,364) 
 *** combined adjacent 142 cells.
[a, b, c, d, e, f],[b, a]
 2>> using Lazard's method (BM20).
[f]
[e]
[d]
[c]
[b,1]
[a,1]
 <<2
time = 35 ms.
1 1(0,0) 1(0,0) 1(0,0) 1(0,0) 1(0,0) 
 *** combined adjacent 0 cells.
0,1,0
[x,3]
[a, b, c, d, e],[b, e*c]
 2>> using Lazard's method (BM20).
[e,1]
[d]
[c,1]
[b,1]
[a]
 <<2
time = 39 ms.
1 1(0,0) 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
[a, b, c, d, e],[a, d*c]
 2>> using Lazard's method (BM20).
[e]
[d,1]
[c,1]
[b]
[a,1]
 <<2
time = 42 ms.
1 1(0,0) 3(0,0) 5(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1,1
[f,3]
[a, b, c, d],[a, d*b]
 2>> using Lazard's method (BM20).
[d,1]
[c]
[b,1]
[a,1]
 <<2
time = 40 ms.
1 3(0,0) 3(0,0) 5(0,0) 
 *** combined adjacent 2 cells.
1
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
 <<1
time = 4,337 ms.
3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1257(0,396) 5800(0,1204) 23424(0,1720) 1(0,0) 
 *** combined adjacent 0 cells.
1[a = [a,1],b = [b,1],c = [c,1],d = [d,1],e = [e,1],f < [f,1],true,true,true]
time = 1,880 ms.

? tst12([all,all,all],[a,b,c,d,e,f,x,y,z],id,"((a*x+b)*y+c)*z+((d*x+e)*y+f)<0",7);Ans()
 *** using the sum of squares projection.
[z,1]
[y,2]
[x,3]
[f,3]
[e,2]
[d,1]
[c,1]
[b,1]
[a,1]
time = 317 ms.
3 9(0,0) 27(0,0) 81(0,0) 291(0,60) 1097(272,386) 4808(0,1204) 13024(2000,1700) 1(0,0) 
 *** combined adjacent 0 cells.
1[a = [a,1],b = [b,1],c = [c,1],d = [d,1],e = [e,1],f < [f,1],true,true,true]
time = 1,724 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[((a*x+b)*y+c)*z+((d*x+e)*y+f)<0,{a,b,c,d,e,f,x,y,z},"Function"];//Timing        

Out[1]= {9.409335, Null}  (* The number of the top level cells is 5323. *)

In[2]:= SetSystemOptions["InequalitySolvingOptions"->{"BrownProjection" -> False, "LazardProjection" -> True}];  

In[3]:= CylindricalDecomposition[((a*x+b)*y+c)*z+((d*x+e)*y+f)<0,{a,b,c,d,e,f,x,y,z},"Function"];//Timing        

Out[3]= {14.773644, Null}  (* The number of the top level cells is 4673. *)

本日のC.A.D.

? tst12([],[c,a,d,b],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2<=a,b^2<=b,c^2<=c,d^2<=d,(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0",17);Ans();
 *** using Lazard's method (BM20).
1
[b,3]
0,0,-5
[d,7]
[a,16]
[c,3]
[[[c-1],[a-1],[],[]],[[c-1],[a+1],[],[]],[[c],[a],[],[]],[[c+1],[a-1],[],[]],[[c+1],[a+1],[],[]]]
time = 2165 ms.
7 145(90,46) 1967(158,205) 16733(2500,1450) 
 *** combined adjacent 16732 cells.
1[true,true,true,true]
time = 3,933 ms.

? tst12([],[a,b,c,d],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2<=a,b^2<=b,c^2<=c,d^2<=d,(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0",17);Ans();
 *** using Lazard's method (BM20).
1
[d,3]
0,0,0
[c,8]
-5,-5,-5,-5,-5,-5,-5,-5,-5,-5,-5,-5
[b,18]
[a,30]
[[[a-1],[b-1],[],[]],[[a],[b],[],[]],[[a+1],[b+1],[],[]]]
time = 2306 ms.
103 5601(74,121) 92535(3000,5402) 794143(64444,37904) 
 *** combined adjacent 794142 cells.
1[true,true,true,true]
time = 3min, 19,428 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[Implies[And[a^2<=a,b^2<=b,c^2<=c,d^2<=d],(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(
c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0],{c,a,d,b},"Function"]//Timing                     

Out[1]= {6.577429, True}

In[2]:= CylindricalDecomposition[Implies[And[a^2<=a,b^2<=b,c^2<=c,d^2<=d],(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(
c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0],{a,b,c,d},"Function"]//Timing                     

Out[2]= {98.025059, True}

G.O.Passmore "Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex"

本日のC.A.D.

? tst12([all,ex],[a,b,x,y],(f1,f2)->f1*f2,"x^6+x*y+a>0,x+b*y^6+a<0",17);Ans()
 *** using Lazard's method (BM20).
1,0
[y,2]
-5
[x,3]
-5
[b,2]
[a,2]
[[[a],[],[x],[]]]
time = 1718 ms.
5 25(0,2) 180(55,29) 113(108,74) 
 *** combined adjacent 88 cells.
1[[a,1] < a,b < [b,1],true,true]
time = 1,264 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[ForAll[x,Exists[y,x^6+x*y+a>0,x+b*y^6+a<0]],{a,b},"Function"]//Timing           

Out[1]= 
{23.867581, CylindricalDecompositionFunction[{CylindricalDecompositionFunction["Variable"][1] > 0 && 
     CylindricalDecompositionFunction["Variable"][2] < 0, {2, 2, 1}, 2657360598}][a, b]}

Thomas Sturm "A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications" において "This instructive example has been used by Hoon Hong in a colloquium talk at the University of Passau in 2005." と紹介されている例の次数を上げたもの.