本日のC.A.D.

A.W.Strzebonski "Cylindrical Algebraic Decomposition using validated numerics" の 7.2. Randomly generated systems で使用された入力です．元の code では CylindricalDecomposition ですが，変数順序を heuristic に委ねるため，無指定の Reduce で実行しました．

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

In[1]:= rana={-363 + 177*x1 - 125*x1*x2^2 + 444*x2^3 - 766*x2*x3 + 477*x1*x2*x3 + 447*x3^2 == 0 && 864 - 55*x1^3*
x2 - 491*x2^2 + 959*x1*x2^3 - 465*x1*x3^2 > 0,566 + 180*x1^2*x2^2 + 264*x1^2*x3 + 919*x2^2*x3 + 941*x2^3*x3 + 481
*x1*x2*x3^2 - 519*x2*x3^3 >= 0,634 - 508*x3 + 896*x3^3 - 342*x1*x2*x4 - 462*x2*x3*x4 + 144*x2*x4^2 >= 0,-120 + 38
*x2^3*x4 + 207*x3*x4 + 872*x3^2*x4 + 165*x2*x3^2*x4 + 672*x2*x3*x4^2 + 87*x3^2*x4^2 == 0,-394 + 902*x2 - 282*x1*x
2 + 347*x3 + 389*x2*x3 - 209*x1*x2*x3 + 987*x2*x3^2 == 0 && -202 + 292*x2^3 + 326*x2^2*x3 + 728*x2*x3^2 - 80*x3^3
 > 0 && -866 - 1024*x1^4 - 886*x2*x3 - 736*x1*x2^2*x3 + 763*x2*x3^3 >= 0};                                       

In[2]:= ranb={446 + 511*x3 - 190*x1^3*x3 + 132*x2^2*x3 + 968*x1^2*x2*x4 + 226*x1*x2*x3*x4 + 645*x2*x3*x4^2 > 0,-4
47 - 312*x3 + 623*x3^2 - 912*x2*x4 + 555*x4^2 == 0 && -730 - 978*x2*x3 + 557*x2*x3^2 + 487*x1^2*x4 - 701*x2*x3*x4
 + 470*x2*x4^2 + 297*x3*x4^2 >= 0,-894 - 884*x2*x3 - 290*x3^2 + 144*x1*x3^2 - 887*x2*x3^2 + 20*x3^3 == 0 && -100 
+ 571*x1*x3 - 314*x2^3*x3 + 398*x1*x3^3 - 522*x2*x3^3 >= 0,505 + 834*x2^3*x3 + 887*x2*x3^2 + 151*x3^3 - 243*x2*x3
^3 == 0 && -323 - 408*x1^2*x2 + 484*x1*x2^2 + 556*x3 + 705*x1*x2*x3 > 0 && 422 - 225*x1^4 + 903*x1^2*x3^2 - 944*x
2^2*x3^2 + 996*x3^4 >= 0,-263 - 172*x2 + 78*x2^2 + 41*x2*x3 + 864*x4 + 623*x2*x4 + 293*x3*x4 > 0 && 781 + 948*x1^
2 - x3 - 946*x1^3*x4 - 606*x1*x3*x4 >= 0};                                                                       

In[3]:= ranc={-417 + 159*x1^3 + 210*x1^3*x2 + 358*x1*x2^2*x3 + 605*x2*x3^3 == 0 && -1016 + 1010*x2 + 516*x1*x2 - 
960*x3 + 571*x1*x3 - x3^2 > 0 && -4 + 627*x1^2 - 100*x1*x2 - 670*x3 + 670*x1*x3 >= 0,-502 - 1013*x1*x2*x3 + 328*x
2^2*x3 + 330*x1*x3^2 + 884*x3*x4 + 502*x1*x3*x4 == 0 && 313 - 636*x2 - 997*x1*x3 - 573*x3^2 + 591*x3*x4 >= 0,790 
+ 446*x2^3 + 189*x1^2*x3 + 399*x1*x2*x3 - 110*x3^2 - 19*x2*x3^2 > 0 && 60 - 531*x1^2 - 691*x1*x2 + 908*x1^2*x3 - 
935*x1*x2*x3 + 431*x2^2*x3 - 747*x3^3 >= 0,275 + 130*x3^2 - 279*x2*x4 - 113*x3*x4 + 620*x4^2 > 0 && 542 + 680*x1*
x3 + 75*x2^2*x3 + 550*x1*x3^2 + 621*x1*x3*x4 >= 0,-218 + 955*x1^2*x2*x3 + 520*x2*x3^3 + 1017*x3^4 + 250*x1*x2*x4 
- 391*x2^3*x4 - 525*x1*x3*x4^2 > 0};                                                                             

In[4]:= First@Timing@Reduce[#,Reals]&/@rana//Timing                                               

Out[4]= {1.426756, {0.467609, 0.346341, 0.038994, 0.43843, 0.134579}}

In[5]:= First@Timing@Reduce[#,Reals]&/@ranb//Timing                                               

Out[5]= {7.619839, {0.886294, 0.062116, 0.02397, 4.808107, 1.835422}}

In[6]:= First@Timing@Reduce[#,Reals]&/@ranc//Timing                                               

Out[6]= {17.547247, {3.909086, 3.40725, 4.59773, 0.081719, 5.538123}}

同じ入力に対する tst12 の実行結果です．

                         GP/PARI CALCULATOR Version 2.14.0 (development git-b0a4238356)
                          amd64 running linux (x86-64/GMP-6.2.1 kernel) 64-bit version
                     compiled: Feb 21 2021, gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04)
                                            threading engine: single
                                 (readline v8.0 enabled, extended help enabled)

                                     Copyright (C) 2000-2021 The PARI Group

PARI/GP is free software, covered by the GNU General Public License, and comes WITHOUT ANY WARRANTY WHATSOEVER.

Type ? for help, \q to quit.
Type ?17 for how to get moral (and possibly technical) support.

parisizemax = 20000002048, primelimit = 500000
? wt=getwalltime();rana7(7*23);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,6],[x2,3,7],[x3,2,4]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x3,2]
[x1,4]
[x2,11]
time = 261 ms.
45 743(16,30) 704(324,304) 
 *** combined adjacent 173 cells.
[[[x1,2,3],[x2,3,5],[x3,3,5]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,1]
[x3,2]
[x2,3]
time = 66 ms.
13 109(8,2) 277(70,0) 
 *** combined adjacent 184 cells.
[[[x1,1,1],[x2,1,3],[x3,3,3],[x4,2,3]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x4,2]
[x3,2]
time = 115 ms.
5 23(0,2) 69(10,10) 98(0,0) 
 *** combined adjacent 44 cells.
[[[x1,0,0],[x2,3,3],[x3,2,5],[x4,2,6]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1]
[x2,1]
[x3,1]
[x4,3]
time = 74 ms.
11 47(8,0) 78(38,0) 78(0,0) 
 *** combined adjacent 13 cells.
[[[x1,4,4],[x2,3,11],[x3,3,10]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,2]
[x3,5]
[x2,10]
time = 1,151 ms.
33 143(16,23) 4(58,6) 
 *** combined adjacent 2 cells.
total = 3,205 ms.

? wt=getwalltime();rana7(7*29);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,4,6],[x2,3,4,7],[x3,2,3,4]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x3,2]
[x1,4]
[x2,11]
time = 230 ms.
45 743(16,30) 704(324,304) 
 *** combined adjacent 173 cells.
[[[x1,2,4,3],[x2,3,4,5],[x3,3,4,5]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,1]
[x3,2]
[x2,3]
time = 66 ms.
13 109(8,2) 277(70,0) 
 *** combined adjacent 184 cells.
[[[x1,1,3,1],[x2,1,3,3],[x3,3,3,3],[x4,2,3,3]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x4,2]
[x3,2]
time = 107 ms.
5 23(0,2) 69(10,10) 98(0,0) 
 *** combined adjacent 44 cells.
[[[x1,0,0,0],[x2,3,4,3],[x3,2,4,5],[x4,2,4,6]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1]
[x2,1]
[x3,1]
[x4,3]
time = 78 ms.
11 47(8,0) 78(38,0) 78(0,0) 
 *** combined adjacent 13 cells.
[[[x1,4,4,4],[x2,3,4,11],[x3,3,4,10]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,2]
[x3,5]
[x2,10]
time = 1,169 ms.
33 143(16,23) 4(58,6) 
 *** combined adjacent 2 cells.
total = 3,205 ms.

? wt=getwalltime();rana7(7*31);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,8,13,18,6],[x2,13,17,21,7],[x3,6,10,10,4]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x3,2]
[x1,4]
[x2,11]
time = 222 ms.
45 743(16,30) 704(324,304) 
 *** combined adjacent 173 cells.
[[[x1,5,8,11,3],[x2,9,11,19,5],[x3,8,11,18,5]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,1]
[x3,2]
[x2,3]
time = 66 ms.
13 109(8,2) 277(70,0) 
 *** combined adjacent 184 cells.
[[[x1,1,2,3,1],[x2,3,2,9,3],[x3,5,6,7,3],[x4,4,5,9,3]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x4,2]
[x3,2]
time = 108 ms.
5 23(0,2) 69(10,10) 98(0,0) 
 *** combined adjacent 44 cells.
[[[x1,0,0,0,0],[x2,5,11,12,3],[x3,8,8,17,5],[x4,8,8,21,6]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1]
[x2,1]
[x3,1]
[x4,3]
time = 72 ms.
11 47(8,0) 78(38,0) 78(0,0) 
 *** combined adjacent 13 cells.
[[[x1,7,14,13,4],[x2,15,16,30,11],[x3,16,22,28,10]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,2]
[x2,5]
[x3,6]
time = 767 ms.
15 55(12,11) 6(26,6) 
 *** combined adjacent 1 cells.
total = 2,406 ms.

? wt=getwalltime();ranb7(7*23);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,3],[x2,2,4],[x3,1,5],[x4,2,3]]]
 *** using the sum of squares projection.
[x4,1]
[x3,3]
[x2,5]
[x1,8]
time = 174 ms.
21 175(12,15) 915(102,86) 1192(390,0) 
 *** combined adjacent 44 cells.
[[[x1,2,1],[x2,1,5],[x3,2,6],[x4,2,6]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x4,5]
[x3,8]
time = 145 ms.
25 195(16,18) 180(0,60) 270(64,0) 
 *** combined adjacent 178 cells.
[[[x1,1,3],[x2,3,4],[x3,3,9]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,2]
[x2,2]
[x3,3]
time = 134 ms.
7 31(4,0) 21(0,24) 
 *** combined adjacent 6 cells.
[[[x1,4,5],[x2,3,7],[x3,4,9]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,2]
[x2,6]
[x3,16]
time = 1,358 ms.
95 152(16,87) 251(14,8) 
 *** combined adjacent 151 cells.
[[[x1,3,3],[x2,2,4],[x3,1,4],[x4,1,5]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x3,2]
[x4,5]
[x2,8]
[x1,21]
time = 311 ms.
75 1681(14,80) 13707(546,668) 13910(0,5540) 
 *** combined adjacent 7087 cells.
total = 10,369 ms.

? wt=getwalltime();ranb7(7*29);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,4,3],[x2,2,4,4],[x3,1,4,5],[x4,2,4,3]]]
 *** using the sum of squares projection.
[x4,1]
[x3,3]
[x2,5]
[x1,8]
time = 174 ms.
21 175(12,15) 915(102,86) 1192(390,0) 
 *** combined adjacent 44 cells.
[[[x1,2,3,1],[x2,1,3,5],[x3,2,3,6],[x4,2,3,6]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x4,5]
[x3,8]
time = 145 ms.
25 195(16,18) 180(0,60) 270(64,0) 
 *** combined adjacent 178 cells.
[[[x1,1,4,3],[x2,3,4,4],[x3,3,4,9]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,2]
[x2,2]
[x3,3]
time = 108 ms.
7 31(4,0) 21(0,24) 
 *** combined adjacent 6 cells.
[[[x1,4,4,5],[x2,3,4,7],[x3,4,4,9]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,2]
[x2,6]
[x3,16]
time = 1,371 ms.
95 152(16,87) 251(14,8) 
 *** combined adjacent 151 cells.
[[[x1,3,4,3],[x2,2,2,4],[x3,1,3,4],[x4,1,4,5]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x3,2]
[x2,3]
[x4,6]
[x1,12]
time = 216 ms.
49 709(4,26) 4191(300,386) 5002(0,2064) 
 *** combined adjacent 2701 cells.
total = 6,579 ms.

? wt=getwalltime();ranb7(7*31);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,6,11,12,3],[x2,5,7,15,4],[x3,5,3,16,5],[x4,4,8,12,3]]]
 *** using the sum of squares projection.
[x4,1]
[x3,3]
[x2,5]
[x1,8]
time = 174 ms.
21 175(12,15) 915(102,86) 1192(390,0) 
 *** combined adjacent 44 cells.
[[[x1,2,5,3,1],[x2,5,3,13,5],[x3,8,7,14,6],[x4,9,7,16,6]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,1]
[x2,2]
[x3,4]
[x4,6]
time = 158 ms.
19 139(20,14) 136(0,52) 218(56,0) 
 *** combined adjacent 124 cells.
[[[x1,3,5,9,3],[x2,6,13,13,4],[x3,18,15,27,9]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,2]
[x2,2]
[x3,3]
time = 113 ms.
7 31(4,0) 21(0,24) 
 *** combined adjacent 6 cells.
[[[x1,10,17,17,5],[x2,11,24,24,7],[x3,19,25,30,9]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,2]
[x2,6]
[x3,16]
time = 1,371 ms.
95 152(16,87) 251(14,8) 
 *** combined adjacent 151 cells.
[[[x1,6,8,9,3],[x2,5,2,7,4],[x3,4,3,8,4],[x4,5,4,12,5]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x2,1]
[x3,2]
[x4,4]
[x1,6]
time = 123 ms.
23 199(4,8) 556(92,48) 1058(228,0) 
 *** combined adjacent 11 cells.
total = 4,510 ms.

? wt=getwalltime();ranc7(7*23);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,8],[x2,2,6],[x3,3,7]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x2,3]
[x3,7]
[x1,22]
time = 385 ms.
87 1795(42,71) 561(314,1257) 
 *** combined adjacent 244 cells.
[[[x1,1,4],[x2,2,3],[x3,2,8],[x4,1,3]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x4,2]
[x2,3]
[x1,4]
[x3,10]
time = 244 ms.
41 245(22,18) 901(276,140) 667(0,506) 
 *** combined adjacent 268 cells.
[[[x1,2,6],[x2,3,6],[x3,3,8]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x1,2]
[x2,4]
[x3,16]
time = 304 ms.
59 675(30,29) 1162(326,306) 
 *** combined adjacent 521 cells.
[[[x1,1,3],[x2,2,2],[x3,2,6],[x4,2,4]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x2,2]
[x1,2]
[x4,4]
[x3,4]
time = 161 ms.
11 53(4,7) 189(0,0) 317(76,64) 
 *** combined adjacent 189 cells.
[[[x1,2,3],[x2,3,4],[x3,4,4],[x4,2,3]]]
 *** reordering by degree.
 *** using the sum of squares projection.
[x4,1]
[x1,3]
[x2,4]
[x3,6]
time = 896 ms.
37 277(21,24) 1677(182,84) 1725(850,0) 
 *** combined adjacent 70 cells.
total = 9,355 ms.

? wt=getwalltime();ranc7(7*29);print("total = ",strtime(getwalltime()-wt),".");print();
[[[x1,3,4,8],[x2,2,4,6],[x3,3,4,7]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x2,3]
[x3,7]
[x1,22]
time = 379 ms.
87 1795(42,71) 561(314,1257) 
 *** combined adjacent 244 cells.
[[[x1,1,3,4],[x2,2,3,3],[x3,2,3,8],[x4,1,3,3]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x4,2]
[x2,3]
[x1,4]
[x3,10]
time = 217 ms.
41 245(22,18) 901(276,140) 667(0,506) 
 *** combined adjacent 268 cells.
[[[x1,2,3,6],[x2,3,3,6],[x3,3,3,8]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x1,2]
[x2,4]
[x3,16]
time = 273 ms.
59 675(30,29) 1162(326,306) 
 *** combined adjacent 521 cells.
[[[x1,1,3,3],[x2,2,3,2],[x3,2,3,6],[x4,2,3,4]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x2,2]
[x1,2]
[x4,4]
[x3,4]
time = 163 ms.
11 53(4,7) 189(0,0) 317(76,64) 
 *** combined adjacent 189 cells.
[[[x1,2,4,3],[x2,3,4,4],[x3,4,4,4],[x4,2,4,3]]]
 *** reordering by d+sotd+o.
 *** using the sum of squares projection.
[x4,1]
[x1,3]
[x2,4]
[x3,6]
time = 886 ms.
37 277(21,24) 1677(182,84) 1725(850,0) 
 *** combined adjacent 70 cells.
total = 9,202 ms.

? wt=getwalltime();ranc7(7*31);print("total = ",strtime(getwalltime()-wt),".");
[[[x1,13,14,21,8],[x2,7,10,17,6],[x3,10,14,16,7]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x2,3]
[x3,7]
[x1,22]
time = 390 ms.
87 1795(42,71) 561(314,1257) 
 *** combined adjacent 244 cells.
[[[x1,4,3,11,4],[x2,4,5,7,3],[x3,10,7,20,8],[x4,3,3,7,3]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x4,2]
[x2,3]
[x1,4]
[x3,10]
time = 222 ms.
41 245(22,18) 901(276,140) 667(0,506) 
 *** combined adjacent 268 cells.
[[[x1,9,10,16,6],[x2,9,11,17,6],[x3,12,11,23,8]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x1,2]
[x2,4]
[x3,16]
time = 321 ms.
59 675(30,29) 1162(326,306) 
 *** combined adjacent 521 cells.
[[[x1,3,2,8,3],[x2,3,6,5,2],[x3,8,7,15,6],[x4,5,4,9,4]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x2,2]
[x1,2]
[x4,4]
[x3,4]
time = 163 ms.
11 53(4,7) 189(0,0) 317(76,64) 
 *** combined adjacent 189 cells.
[[[x1,4,8,11,3],[x2,6,11,15,4],[x3,9,12,16,4],[x4,4,8,11,3]]]
 *** reordering by sum(d+td in terms)+o.
 *** using the sum of squares projection.
[x4,1]
[x1,3]
[x2,4]
[x3,6]
time = 874 ms.
37 277(21,24) 1677(182,84) 1725(850,0) 
 *** combined adjacent 70 cells.
total = 9,311 ms.