search

sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.5k stars 490 forks source link

Meta-ticket: SAT and SMT #19000

Open rwst opened 9 years ago

rwst commented 9 years ago

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.

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

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

Tickets:

CC: @kcrisman @nbruin @slel

Component: symbolics

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

rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -1 +1,8 @@
 This ticket collects tickets necessary to replace 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.
+
+https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
+http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf
+https://github.com/Z3Prover/z3
+https://github.com/smtrat/smtrat
+https://github.com/pysmt/pysmt
+
rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -1,4 +1,11 @@
 This ticket collects tickets necessary to replace 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 Sage 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.0-r10.12.21.pdf
rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -1,7 +1,7 @@
 This ticket collects tickets necessary to replace 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 Sage problems
+* - SMT-solver benchmark on typical solved and unsolved (by Maxima) problems
 * - SMT-LIB interface
 * - experimental SMT-solver package
rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -8,7 +8,7 @@
 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.0-r10.12.21.pdf
+http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf
 https://github.com/Z3Prover/z3
 https://github.com/smtrat/smtrat
 https://github.com/pysmt/pysmt
rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -1,4 +1,4 @@
-This ticket collects tickets necessary to replace 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.
+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
rwst commented 9 years ago
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(?).

rwst commented 9 years ago

Description changed:

--- 
+++ 
@@ -13,3 +13,4 @@
 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.
rwst commented 8 years ago

Description changed:

--- 
+++ 
@@ -7,10 +7,10 @@

 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://github.com/Z3Prover/z3
-https://github.com/smtrat/smtrat
-https://github.com/pysmt/pysmt
+* https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
+* http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf
+* 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.
rwst commented 8 years ago

Description changed:

--- 
+++ 
@@ -9,6 +9,7 @@

 * 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
dimpase commented 5 years ago
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).

mkoeppe commented 2 years ago

Description changed:

--- 
+++ 
@@ -10,7 +10,7 @@
 * 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
+* #33184: https://github.com/Z3Prover/z3
 * https://github.com/smtrat/smtrat
 * https://github.com/pysmt/pysmt
mkoeppe commented 2 years ago

Description changed:

--- 
+++ 
@@ -10,8 +10,13 @@
 * 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
-* #33184: 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.
+
+Tickets:
+- #33162/#33183/#25374 cryptominisat/pycryptosat fix/update
+- #33184: https://github.com/Z3Prover/z3
+
+