Opened 5 years ago
Last modified 19 months ago
#19000 new enhancement
SMT-solve metaticket
Reported by: | rws | Owned by: | |
---|---|---|---|
Priority: | major | Milestone: | sage-feature |
Component: | symbolics | Keywords: | |
Cc: | kcrisman, nbruin, slelievre | Merged in: | |
Authors: | Reviewers: | ||
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | Stopgaps: |
Description (last modified by )
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.
- #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/Z3Prover/z3
- 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.
Change History (10)
comment:1 Changed 5 years ago by
- Description modified (diff)
comment:2 Changed 5 years ago by
- Description modified (diff)
comment:3 Changed 5 years ago by
- Cc kcrisman nbruin added
- Description modified (diff)
comment:4 Changed 5 years ago by
- Description modified (diff)
comment:5 Changed 5 years ago by
- Description modified (diff)
- Milestone changed from sage-6.9 to sage-feature
comment:6 Changed 5 years ago by
- Description modified (diff)
comment:7 Changed 5 years ago by
- Cc slelievre added
comment:8 Changed 4 years ago by
- Description modified (diff)
comment:9 Changed 4 years ago by
- Description modified (diff)
comment:10 Changed 19 months ago by
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).
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(?).