Abstract SAT Solver#

All SAT solvers must inherit from this class.

Note

Our SAT solver interfaces are 1-based, i.e., literals start at 1. This is consistent with the popular DIMACS format for SAT solving but not with Python’s 0-based convention. However, this also allows to construct clauses using simple integers.

AUTHORS:

  • Martin Albrecht (2012): first version

sage.sat.solvers.satsolver.SAT(solver=None, *args, **kwds)[source]#

Return a SatSolver instance.

Through this class, one can define and solve SAT problems.

INPUT:

  • solver (string) – select a solver. Admissible values are:

    • "cryptominisat" – note that the pycryptosat package must be installed.

    • "picosat" – note that the pycosat package must be installed.

    • "glucose" – note that the glucose package must be installed.

    • "glucose-syrup" – note that the glucose package must be installed.

    • "LP" – use SatLP to solve the SAT instance.

    • None (default) – use CryptoMiniSat if available, else PicoSAT if available, and a LP solver otherwise.

EXAMPLES:

sage: SAT(solver="LP")                                                          # needs sage.numerical.mip
an ILP-based SAT Solver

>>> from sage.all import *
>>> SAT(solver="LP")                                                          # needs sage.numerical.mip
an ILP-based SAT Solver
class sage.sat.solvers.satsolver.SatSolver#

Bases: object

add_clause(lits)[source]#

Add a new clause to set of clauses.

INPUT:

  • lits – a tuple of integers != 0

Note

If any element e in lits has abs(e) greater than the number of variables generated so far, then new variables are created automatically.

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.add_clause( (1, -2 , 3) )
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.add_clause( (Integer(1), -Integer(2) , Integer(3)) )
Traceback (most recent call last):
...
NotImplementedError
clauses(filename=None)[source]#

Return original clauses.

INPUT:

  • filename'' -- if not ``None clauses are written to filename in DIMACS format (default: None)

OUTPUT:

If filename is None then a list of lits, is_xor, rhs tuples is returned, where lits is a tuple of literals, is_xor is always False and rhs is always None.

If filename points to a writable file, then the list of original clauses is written to that file in DIMACS format.

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.clauses()
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.clauses()
Traceback (most recent call last):
...
NotImplementedError
conflict_clause()[source]#

Return conflict clause if this instance is UNSAT and the last call used assumptions.

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.conflict_clause()
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.conflict_clause()
Traceback (most recent call last):
...
NotImplementedError
learnt_clauses(unitary_only=False)[source]#

Return learnt clauses.

INPUT:

  • unitary_only – return only unitary learnt clauses (default: False)

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.learnt_clauses()
Traceback (most recent call last):
...
NotImplementedError

sage: solver.learnt_clauses(unitary_only=True)
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.learnt_clauses()
Traceback (most recent call last):
...
NotImplementedError

>>> solver.learnt_clauses(unitary_only=True)
Traceback (most recent call last):
...
NotImplementedError
nvars()[source]#

Return the number of variables.

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.nvars()
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.nvars()
Traceback (most recent call last):
...
NotImplementedError
read(filename)[source]#

Reads DIMAC files.

Reads in DIMAC formatted lines (lazily) from a file or file object and adds the corresponding clauses into this solver instance. Note that the DIMACS format is not well specified, see http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html, http://www.satcompetition.org/2009/format-benchmarks2009.html, and http://elis.dvo.ru/~lab_11/glpk-doc/cnfsat.pdf.

The differences were summarized in the discussion on the issue Issue #16924. This method assumes the following DIMACS format:

  • Any line starting with “c” is a comment

  • Any line starting with “p” is a header

  • Any variable 1-n can be used

  • Every line containing a clause must end with a “0”

The format is extended to allow lines starting with “x” defining xor clauses, with the notation introduced in cryptominisat, see https://www.msoos.org/xor-clauses/

INPUT:

  • filename – The name of a file as a string or a file object

EXAMPLES:

sage: from io import StringIO
sage: file_object = StringIO("c A sample .cnf file.\np cnf 3 2\n1 -3 0\n2 3 -1 0 ")
sage: from sage.sat.solvers.dimacs import DIMACS
sage: solver = DIMACS()
sage: solver.read(file_object)
sage: solver.clauses()
[((1, -3), False, None), ((2, 3, -1), False, None)]

>>> from sage.all import *
>>> from io import StringIO
>>> file_object = StringIO("c A sample .cnf file.\np cnf 3 2\n1 -3 0\n2 3 -1 0 ")
>>> from sage.sat.solvers.dimacs import DIMACS
>>> solver = DIMACS()
>>> solver.read(file_object)
>>> solver.clauses()
[((1, -3), False, None), ((2, 3, -1), False, None)]

With xor clauses:

sage: from io import StringIO
sage: file_object = StringIO("c A sample .cnf file with xor clauses.\np cnf 3 3\n1 2 0\n3 0\nx1 2 3 0")
sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat          # optional - pycryptosat
sage: solver = CryptoMiniSat()                                          # optional - pycryptosat
sage: solver.read(file_object)                                          # optional - pycryptosat
sage: solver.clauses()                                                  # optional - pycryptosat
[((1, 2), False, None), ((3,), False, None), ((1, 2, 3), True, True)]
sage: solver()                                                          # optional - pycryptosat
(None, True, True, True)

>>> from sage.all import *
>>> from io import StringIO
>>> file_object = StringIO("c A sample .cnf file with xor clauses.\np cnf 3 3\n1 2 0\n3 0\nx1 2 3 0")
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat          # optional - pycryptosat
>>> solver = CryptoMiniSat()                                          # optional - pycryptosat
>>> solver.read(file_object)                                          # optional - pycryptosat
>>> solver.clauses()                                                  # optional - pycryptosat
[((1, 2), False, None), ((3,), False, None), ((1, 2, 3), True, True)]
>>> solver()                                                          # optional - pycryptosat
(None, True, True, True)
var(decision=None)[source]#

Return a new variable.

INPUT:

  • decision – is this variable a decision variable?

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.var()
Traceback (most recent call last):
...
NotImplementedError

>>> from sage.all import *
>>> from sage.sat.solvers.satsolver import SatSolver
>>> solver = SatSolver()
>>> solver.var()
Traceback (most recent call last):
...
NotImplementedError