#11479: SAT Solver Interface
------------------------+---------------------------------------------------
Reporter: fichtejo | Owner: jason
Type: task | Status: new
Priority: minor | Milestone: sage-4.7.1
Component: misc | Keywords:
Work_issues: | Upstream: N/A
Reviewer: | Author: Johannes Fichte
Merged: | Dependencies:
------------------------+---------------------------------------------------
Since sage does not have any boolean satisfiablity support, we should
change this :-)
Implement a simple interface to SAT solvers:
Ideas:
1) Data structures
- clauses
- cnf formulas (implements DIMACS converting...)
- results
2) Additional features to CNF class
- various implementations of at most k variables are true
3) Some examples
- e.g., Sudoku, vertex cover via binary search
4) Solver shell/string parsing interface for:
- MiniSAT
- RSAT
- Berkmin
- Siege
- zChaff
Further ideas:
5) direct C++ Interface (suggested by Martin)
- MiniSAT
- RSAT
- CryptMiniSat
Some ideas are attached:
- sat.py implements
- Clause (set of integers inherits from set)
- CNFFormula (list of Clauses)
- features:
- create DIMACS
- read from DIMACS
- is_satisfiable (calls sat solver)
- solve (calls sat solver and returns additional information),
next step: obtain satisfiable assignments from solvers
- is_horn (do we have HORN clauses only)
- is_2cnf (do we have 2 CNF clauses only)
- at_most_k_variables_true (adds clauses such that at most k
variables are true)
- backend.py
- SolverResult (simple result class, needs improvement)
- Solver (call SAT solver, process string solver result)
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/11479>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
