Opened 4 years ago
Last modified 2 years 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 (9)
comment:1 Changed 4 years ago by
- Description modified (diff)
comment:2 Changed 4 years ago by
- Description modified (diff)
comment:3 Changed 4 years ago by
- Cc kcrisman nbruin added
- Description modified (diff)
comment:4 Changed 4 years ago by
- Description modified (diff)
comment:5 Changed 4 years ago by
- Description modified (diff)
- Milestone changed from sage-6.9 to sage-feature
comment:6 Changed 4 years ago by
- Description modified (diff)
comment:7 Changed 3 years ago by
- Cc slelievre added
comment:8 Changed 2 years ago by
- Description modified (diff)
comment:9 Changed 2 years ago by
- Description modified (diff)
Note: See
TracTickets for help on using
tickets.
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(?).