SAT-Solvers via DIMACS Files¶
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 and Glucose 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:
Martin Albrecht (2012): first version
Classes and Methods¶
- class sage.sat.solvers.dimacs.DIMACS(command=None, filename=None, verbosity=0, **kwds)¶
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.
- __init__(command=None, filename=None, verbosity=0, **kwds)¶
Construct a new generic DIMACS solver.
INPUT:
command
- a named format string with the command to run. The string must contain {input} and may contain {output} if the solvers writes the solution to an output file. For example “sat-solver {input}” is a valid command. IfNone
then the class variablecommand
is used. (default:None
)filename
- a filename to write clauses to in DIMACS format, must be writable. IfNone
a temporary filename is chosen automatically. (default:None
)verbosity
- a verbosity level, where zero means silent and anything else means verbose output. (default:0
)**kwds
- accepted for compatibility with other solves, ignored.
- __call__(assumptions=None)¶
Run ‘command’ and collect output.
INPUT:
assumptions
- ignored, accepted for compatibility with other solvers (default:None
)
- 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.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: ''
- clauses(filename=None)¶
Return original clauses.
INPUT:
filename
- if notNone
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.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
- nvars()¶
Return the number of variables.
EXAMPLES:
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
- static render_dimacs(clauses, filename, nlits)¶
Produce DIMACS file
filename
fromclauses
.INPUT:
clauses
- a list of clauses, either in simple format as a list of literals or in extended format for CryptoMiniSat: a tuple of literals,is_xor
andrhs
.filename
- the file to write tonlits -- the number of literals appearing in ``clauses
EXAMPLES:
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
- var(decision=None)¶
Return a new variable.
INPUT:
decision
- accepted for compatibility with other solvers, ignored.
EXAMPLES:
sage: from sage.sat.solvers.dimacs import DIMACS sage: solver = DIMACS() sage: solver.var() 1
- write(filename=None)¶
Write DIMACS file.
INPUT:
filename
- ifNone
default filename specified at initialization is used for writing to (default:None
)
EXAMPLES:
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
- class sage.sat.solvers.dimacs.Glucose(command=None, filename=None, verbosity=0, **kwds)¶
Bases:
sage.sat.solvers.dimacs.DIMACS
An instance of the Glucose solver.
For information on Glucose see: http://www.labri.fr/perso/lsimon/glucose/
EXAMPLES:
sage: from sage.sat.solvers import Glucose sage: solver = Glucose() sage: solver DIMACS Solver: 'glucose -verb=2 {input} {output}' sage: solver.add_clause( (1, 2, 3) ) sage: solver.add_clause( (-1,) ) sage: solver.add_clause( (-2,) ) sage: solver() # optional - glucose (None, False, False, True)
- class sage.sat.solvers.dimacs.GlucoseSyrup(command=None, filename=None, verbosity=0, **kwds)¶
Bases:
sage.sat.solvers.dimacs.DIMACS
An instance of the Glucose-syrup parallel solver.
For information on Glucose see: http://www.labri.fr/perso/lsimon/glucose/
- class sage.sat.solvers.dimacs.RSat(command=None, filename=None, verbosity=0, **kwds)¶
Bases:
sage.sat.solvers.dimacs.DIMACS
An instance of the RSat solver.
For information on RSat see: http://reasoning.cs.ucla.edu/rsat/