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:

Status badges

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)

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)

backend.py (14.9 KB) - added by fichtejo 10 years ago.
Basic backend
sat.py (28.8 KB) - added by fichtejo 10 years ago.
Clause, CNFFormula
minisat.py (7.7 KB) - added by fichtejo 10 years ago.
String Processing for MiniSAT

Download all attachments as: .zip

Change History (19)

Changed 10 years ago by fichtejo

Basic backend

Changed 10 years ago by fichtejo

Clause, CNFFormula

Changed 10 years ago by fichtejo

String Processing for MiniSAT

comment:1 Changed 10 years ago by tmonteil

  • Cc tmonteil added

comment:2 follow-up: Changed 9 years ago by was

See also #418.

comment:3 in reply to: ↑ 2 Changed 9 years ago by kcrisman

See also #418.

Given recent activity there, is this a dup? Of course, there is code here (and #11479) which could be useful, so I won't make that call.

comment:4 Changed 9 years ago by fichtejo

#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 malb

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 malb

I added DIMACS solvers to #418.

comment:7 Changed 9 years ago by malb

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 jdemeyer

  • Milestone changed from sage-5.11 to sage-5.12

comment:9 Changed 7 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:10 Changed 7 years ago by mmezzarobba

  • 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: Changed 7 years ago by malb

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: Changed 7 years ago by 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?

comment:13 in reply to: ↑ 12 Changed 7 years ago by mmezzarobba

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 ncohen

Oh. PLease add me in CC of any sat-related ticket you might create :-)

Nathann

comment:15 Changed 7 years ago by ncohen

  • Status changed from needs_review to positive_review

comment:16 Changed 7 years ago by vbraun

  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.