Opened 10 years ago
Closed 7 years ago
#11479 closed task (fixed)
SAT Solver Interface
Reported by: | fichtejo | Owned by: | jason |
---|---|---|---|
Priority: | minor | Milestone: | sage-duplicate/invalid/wontfix |
Component: | misc | Keywords: | |
Cc: | malb, ncohen, schilly, tmonteil | Merged in: | |
Authors: | Johannes Fichte | Reviewers: | |
Report Upstream: | N/A | Work issues: | |
Branch: | Commit: | ||
Dependencies: | Stopgaps: |
Description
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)
Attachments (3)
Change History (19)
Changed 10 years ago by
comment:1 Changed 10 years ago by
- Cc tmonteil added
comment:2 follow-up: ↓ 3 Changed 9 years ago by
See also #418.
comment:3 in reply to: ↑ 2 Changed 9 years ago by
comment:4 Changed 9 years ago by
#418 interacts only with cryptominisat. #5671 gives a wrapper for miniSAT. RSat and others are still interesting. I suggested here to create a common wrapper for many solvers, but also to create a string-based interface (create DIMACS and parse output) for solvers that are neither open source nor provide a wrapper. I think we should merge the work.
comment:5 Changed 9 years ago by
Agreed! I started from scratch because it was simpler for me but we should merge. Perhaps you could add a "DIMACS" solver to sage.sat.solvers which would understand the same commands as my cryptominisat solver interface (which we can change to suite your needs as well). This way my higher level code would still be applicable, e.g., the ANF to CNF conversion and the solve() function?
comment:6 Changed 9 years ago by
I added DIMACS solvers to #418.
comment:7 Changed 9 years ago by
What are we going to do with this ticket? There hasn't been any movement in months and there's #418? Close it?
comment:8 Changed 8 years ago by
- Milestone changed from sage-5.11 to sage-5.12
comment:9 Changed 7 years ago by
- Milestone changed from sage-6.1 to sage-6.2
comment:10 Changed 7 years ago by
- Milestone changed from sage-6.2 to sage-duplicate/invalid/wontfix
- Status changed from new to needs_review
Most of the suggested features now seem to be available in sage.sat
, but some ideas may still be relevant. What do people think?
comment:11 follow-up: ↓ 12 Changed 7 years ago by
Wouldn't it be better to open a new ticket for (each of) the features that you consider missing from sage.sat
?
comment:12 in reply to: ↑ 11 ; follow-up: ↓ 13 Changed 7 years ago by
Wouldn't it be better to open a new ticket for (each of) the features that you consider missing from
sage.sat
?
I agree. With that in mind, let's also close #5671 and open new tickets for new features. mmezzarobba, is that okay?
comment:13 in reply to: ↑ 12 Changed 7 years ago by
Replying to kcrisman:
Wouldn't it be better to open a new ticket for (each of) the features that you consider missing from
sage.sat
?I agree. With that in mind, let's also close #5671 and open new tickets for new features. mmezzarobba, is that okay?
Sorry, apparently I wasn't clear: I was actually suggesting to close this ticket (hence the change to the milestone field), and I don't feel a need for new tickets about the ideas listed here, but I thought some of the ticket's participants might.
comment:14 Changed 7 years ago by
Oh. PLease add me in CC of any sat-related ticket you might create :-)
Nathann
comment:15 Changed 7 years ago by
- Status changed from needs_review to positive_review
comment:16 Changed 7 years ago by
- Resolution set to fixed
- Status changed from positive_review to closed
Basic backend