Sage supports calling SAT solvers using the popular DIMACS format. This module implements infrastructure to make it easy to add new such interfaces and some example interfaces.
Currently, interfaces to RSat [RS] and Glucose [GL] are included by default.
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:
Bases: sage.sat.solvers.satsolver.SatSolver
Generic DIMACS Solver.
Note
Usually, users won’t have to use this class directly but some class which inherits from this class.
Construct a new generic DIMACS solver.
INPUT:
TESTS:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: DIMACS()
DIMACS Solver: ''
Run ‘command’ and collect output.
INPUT:
TESTS:
This class is not meant to be called directly:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: solver.add_clause( (1, -2 , 3) )
sage: solver()
Traceback (most recent call last):
...
ValueError: No SAT solver command selected.
Add a new clause to set of clauses.
INPUT:
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.
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: solver = DIMACS()
sage: solver.var()
1
sage: solver.var(decision=True)
2
sage: solver.add_clause( (1, -2 , 3) )
sage: solver
DIMACS Solver: ''
Return original clauses.
INPUT:
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.
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS()
sage: solver.add_clause( (1, 2, 3) )
sage: solver.clauses()
[((1, 2, 3), False, None)]
sage: solver.add_clause( (1, 2, -3) )
sage: solver.clauses(fn)
sage: print open(fn).read()
p cnf 3 2
1 2 3 0
1 2 -3 0
Return the number of variables.
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: solver = DIMACS()
sage: solver.var()
1
sage: solver.var(decision=True)
2
sage: solver.nvars()
2
Produce DIMACS file filename from clauses.
INPUT:
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS()
sage: solver.add_clause( (1, 2, -3) )
sage: DIMACS.render_dimacs(solver.clauses(), fn, solver.nvars())
sage: print open(fn).read()
p cnf 3 1
1 2 -3 0
This is equivalent to:
sage: solver.clauses(fn)
sage: print open(fn).read()
p cnf 3 1
1 2 -3 0
This function also accepts a “simple” format:
sage: DIMACS.render_dimacs([ (1,2), (1,2,-3) ], fn, 3)
sage: print open(fn).read()
p cnf 3 2
1 2 0
1 2 -3 0
Return a new variable.
INPUT:
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: solver = DIMACS()
sage: solver.var()
1
Write DIMACS file.
INPUT:
EXAMPLE:
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: solver.add_clause( (1, -2 , 3) )
sage: _ = solver.write()
sage: for line in open(fn).readlines():
... print line,
p cnf 3 1
1 -2 3 0
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS()
sage: solver.add_clause( (1, -2 , 3) )
sage: _ = solver.write(fn)
sage: for line in open(fn).readlines():
... print line,
p cnf 3 1
1 -2 3 0
Bases: sage.sat.solvers.dimacs.DIMACS
An instance of the Glucose solver.
For information on Glucose see: http://www.lri.fr/~simon/?page=glucose
Bases: sage.sat.solvers.dimacs.DIMACS
An instance of the RSat solver.
For information on RSat see: http://reasoning.cs.ucla.edu/rsat/