Opened 4 years ago

Last modified 2 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 rws)

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.

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 4 years ago by rws

  • Description modified (diff)

comment:2 Changed 4 years ago by rws

  • Description modified (diff)

comment:3 Changed 4 years ago by rws

  • Cc kcrisman nbruin added
  • Description modified (diff)

comment:4 Changed 4 years ago by rws

  • Description modified (diff)

comment:5 Changed 4 years ago by rws

  • Description modified (diff)
  • Milestone changed from sage-6.9 to sage-feature

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(?).

comment:6 Changed 4 years ago by rws

  • Description modified (diff)

comment:7 Changed 4 years ago by slelievre

  • Cc slelievre added

comment:8 Changed 3 years ago by rws

  • Description modified (diff)

comment:9 Changed 3 years ago by rws

  • Description modified (diff)

comment:10 Changed 2 months ago by dimpase

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).

Note: See TracTickets for help on using tickets.