Abstract SAT Solver¶
All SAT solvers must inherit from this class.
Note
Our SAT solver interfaces are 1based, i.e., literals start at 1. This is consistent with the popular DIMACS format for SAT solving but not with Pythion’s 0based 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."glucosesyrup"
– note that the glucose package must be installed."LP"
– useSatLP
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 ILPbased 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
inlits
hasabs(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 tofilename
in DIMACS format (default:None
)
OUTPUT:
If
filename
isNone
then a list oflits, is_xor, rhs
tuples is returned, wherelits
is a tuple of literals,is_xor
is alwaysFalse
andrhs
is alwaysNone
.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/formatbenchmarks2009.html, and http://elis.dvo.ru/~lab_11/glpkdoc/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 1n 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/xorclauses/INPUT:
filename
 The name of a file as a string or a file object
EXAMPLES:
sage: from six import StringIO # for python 2/3 support 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 six import StringIO # for python 2/3 support 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
