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 Pythion’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)

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 cryptominisat 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")
an ILP-based SAT Solver
class sage.sat.solvers.satsolver.SatSolver

Bases: object

add_clause(lits)

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
clauses(filename=None)

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
conflict_clause()

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
learnt_clauses(unitary_only=False)

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
nvars()

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
read(filename)

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 ticket trac ticket #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)]

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 - cryptominisat
sage: solver = CryptoMiniSat()                                          # optional - cryptominisat
sage: solver.read(file_object)                                          # optional - cryptominisat
sage: solver.clauses()                                                  # optional - cryptominisat
[((1, 2), False, None), ((3,), False, None), ((1, 2, 3), True, True)]
sage: solver()                                                          # optional - cryptominisat
(None, True, True, True)
trait_names()

Allow alias to appear in tab completion.

EXAMPLES:

sage: from sage.sat.solvers.satsolver import SatSolver
sage: solver = SatSolver()
sage: solver.trait_names()
['gens']
var(decision=None)

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