I guess many have heard of the existential theory of the reals:


I have read in various papers that the problem lies in PSPACE. I have frequently some problems that I would like to solve by some of these algorithms. As I am often concerned with small finite instances I don't mind if the computation takes several days. Can someone recommend me a usable implementation?

Preferably, non-commercial.

Apparently SAGE has only a "use at your own risk" version.

Also I am not interested in numerical solutions.

best Till

  • $\begingroup$ Algebraic Geometry??? $\endgroup$
    – abx
    Feb 9, 2017 at 17:21
  • 5
    $\begingroup$ @abx, the tag is appropriate: this is looking for implemented algorithms in real algebraic geometry $\endgroup$
    – Matt F.
    Feb 9, 2017 at 17:41
  • $\begingroup$ Seems promising, but I am not certain of its relevance: Gao, Sicun, Soonho Kong, and Edmund M. Clarke. "dReal: An SMT solver for nonlinear theories over the reals." International Conference on Automated Deduction. Springer Berlin Heidelberg, 2013. Journal link $\endgroup$ Feb 9, 2017 at 18:17
  • 1
    $\begingroup$ I guess a list of SMT-solvers can be found here: en.wikipedia.org/wiki/Satisfiability_modulo_theories . However I have not found one that uses cylindrical algebraic decompositions. Has anyone experience with those solvers for ETR? $\endgroup$
    – Till
    Feb 10, 2017 at 15:12
  • 1
    $\begingroup$ QEPCAD implements cylindrical algebraic decompositions: usna.edu/CS/qepcadweb/B/QEPCAD.html $\endgroup$
    – Tadashi
    Feb 10, 2017 at 21:04


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.