Advanced Search
All Posts :

Consider the following two systems over the reals:

sys__1:=(r*(387*r+52)+2<r*(226*q+121*s)+9*q*(q*(2*q-5)-3*s+2)+6*s,4*q**3+r*(27*r+4)+s**2=q*(q+18*r),q>=0,r>=0):
sys__2:=((392-1739*q)*r+4*(2-9*q)**2+2151*r**2<75*r*s,4*q**3+r*(27*r+4)+s**2=q*(q+18*r),q>=0,r>=0):

The following results indicate that both sys__1 and sys__2 are satisfiable 

QuantifierElimination:-QuantifierEliminate(exists([s,q,r],And(sys__1)));
                              true

QuantifierElimination:-QuantifierEliminate(exists([s,q,r],And(sys__1)));
                              true

but RealDomain:-solve simply returns an empty list (that is, no solution exists) in both cases

RealDomain:-solve(And(sys__1),[q,s,r]); # thus sys1 cannot be satisfied
                               []

RealDomain:-solve(And(sys__2),[q,s,r]); # thus sys2 cannot be satisfied
                               []

Evidently, the above two results conflict with each other, which suggests that there must be a bug in one of these two functions. 
As discussed in the previous problem, the use of RealDomain:-solve is unsafe, Nevertheless, it appears that using QuantifierElimination:-QuantifierEliminate is still not always safe (since the unsatisfiability is also checked by another software). 

Updated. The “inconsistency” problem still exists in Maple 2025: 
 

> 

restart;
> 

kernelopts('version');

`Maple 2025.1, X86 64 WINDOWS, Jun 12 2025, Build ID 1932578`

 (1)
> 

`#msub(mi("sys"),mi("1"))` := r*(387*r+52)+2 < r*(226*q+121*s)+9*q*(q*(2*q-5)-3*s+2)+6*s, 4*q^3+r*(27*r+4)+s^2 = q*(q+18*r), q >= 0, r >= 0
> 

`#msub(mi("sys"),mi("2"))` := (392-1739*q)*r+4*(2-9*q)^2+2151*r^2 < 75*r*s, 4*q^3+r*(27*r+4)+s^2 = q*(q+18*r), q >= 0, r >= 0
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(`&E`([q, r]), `&and`(sys__1))
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(`&E`([q, r]), `&and`(sys__2))

false

  

false

 (2)
> 

QuantifierElimination:-QuantifierEliminate(exists([q, r], And(sys__1)))
> 

QuantifierElimination:-QuantifierEliminate(exists([q, r], And(sys__2)))

s-RootOf(27*_Z^3-216*_Z^2+9*_Z+1, 17498784809929/2199023255552 .. 139990278479459/17592186044416) = 0

  

s-RootOf(13500*_Z^2-210681*_Z-9826, 144368837035598577819/9223372036854775808 .. 288737674071197155665/18446744073709551616) = 0

 (3)
> 

NULL


 

Download 239277-Which-Function-Is-More-Credible.mw

Please Wait...