SAT Solver Interface

[75e7fb91-3597-4c8d-83a5-ad18747e8640]

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)

CC: @malb @nathanncohen @haraldschilly @sagetrac-tmonteil

Component: misc

Author: Johannes Fichte

Issue created by migration from https://trac.sagemath.org/ticket/11479

[75e7fb91-3597-4c8d-83a5-ad18747e8640]

Attachment: backend.py.gz

Basic backend

[75e7fb91-3597-4c8d-83a5-ad18747e8640]

Clause, CNFFormula

[75e7fb91-3597-4c8d-83a5-ad18747e8640]

Attachment: sat.py.gz

String Processing for MiniSAT

[edd8e884-f507-429a-b577-5d554626c0fe]

comment:1

Attachment: minisat.py.gz

[williamstein]

comment:2

See also #418.

[kcrisman]

comment:3

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.

[75e7fb91-3597-4c8d-83a5-ad18747e8640]

comment:4

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.

[malb]

comment:5

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?

[malb]

comment:6

I added DIMACS solvers to !#418.

[malb]

comment:7

What are we going to do with this ticket? There hasn't been any movement in months and there's #418? Close it?

[mezzarobba]

comment:10

Most of the suggested features now seem to be available in sage.sat, but some ideas may still be relevant. What do people think?

[malb]

comment:11

Wouldn't it be better to open a new ticket for (each of) the features that you consider missing from sage.sat?

[kcrisman]

comment:12

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?

[mezzarobba]

comment:13

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.

[6bdad4c1-1e26-4f2f-a442-a01a2292c181]

comment:14

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

Nathann