本日の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." と紹介されている例の次数を上げたもの.