Opened 9 years ago
Last modified 8 years ago
#15680 new enhancement
Using SAT solver module from Symbolic Logic module
Reported by: | equaeghe | Owned by: | |
---|---|---|---|
Priority: | minor | Milestone: | sage-6.4 |
Component: | misc | Keywords: | |
Cc: | malb | Merged in: | |
Authors: | Reviewers: | ||
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | Stopgaps: |
Description
It seems (but I am not entirely sure) that currently the Symbolic Logic module does not (optionally) use the SAT solver module for the is_satisfiable()
method. As this can make this method more efficient, it can be a useful addition. (And allow returning a satisfying instance of the variables.)
(N.B.: Both modules seem to have a method outputting DIMACS format.)
Links:
- related ticket (concerns efficient CNF encoding): http://trac.sagemath.org/ticket/15676
- symbolic logic docs: http://www.sagemath.org/doc/reference/logic/sage/logic/boolformula.html
- SAT solver docs: http://www.sagemath.org/doc/reference/sat
Change History (4)
comment:1 Changed 9 years ago by
- Cc malb added
comment:2 Changed 9 years ago by
- Milestone changed from sage-6.1 to sage-6.2
comment:3 Changed 8 years ago by
- Milestone changed from sage-6.2 to sage-6.3
comment:4 Changed 8 years ago by
- Milestone changed from sage-6.3 to sage-6.4
Note: See
TracTickets for help on using
tickets.