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)#
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"
– 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 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
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/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 - 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)
- 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