Meta-ticket: SAT and SMT

[rwst]

This ticket collects tickets necessary to strengthen Maxima solve with a state-of-the-art SMT-solver. The interface will be the open SMT-LIB 2.0 and so there is a wide choice of packages of which Z3 certainly is the best at the moment.

• basic assumptions on symbolic functions #18999 - add assumptions on defined/hard-coded functions
• • SMT-solver benchmark on typical solved and unsolved (by Maxima) problems
• • SMT-LIB interface
• • experimental SMT-solver package

Pynac will have access to Sage assumptions with version 0.4.3 but the kind of solver is irrelevant with this.

• https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
• http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf
• https://arxiv.org/abs/1607.06945
• https://github.com/smtrat/smtrat
• https://github.com/pysmt/pysmt

Solving with SMT solvers rather means proving satisfiablity, in which they are very good. They also can give an example solution.

Tickets:

• Fix installation of cryptominisat and pycryptosat #33162/Better fix installation of cryptominisat and pycryptosat #33183/Upgrade cryptominisat to 5.8.0, fix build on Cygwin #25374 cryptominisat/pycryptosat fix/update
• Add package z3 #33184: https://github.com/Z3Prover/z3

CC: @kcrisman @nbruin @slel

Component: symbolics

Issue created by migration from https://trac.sagemath.org/ticket/19000

[rwst]

comment:5

Actually I overestimated the capabilities of SMT-solvers. While nice for proving unsat/sat they have no ready-made functionality for complex numbers and Z3 does not return the full solution set but example values that satisy the assertions. But maybe I do not understand how to get this(?).

[dimpase]

comment:10

SMT is quantifier elimination with booleans. Here one really needs quantifier elimination in other, more complicated, 1st order theories (pardon the logic terminology).
While algorithms are known how to do quantifier elimination with complex and reals (assuming the only functions involved are polynomials, otherwise it's harder, or even algorithmically unsolvable), there are not really any off the shelf OSS for this.
(Sage includes qepcad to do this over reals, but it's not so easy to use and very slow).