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

  • Sébastien Labbé (2018): adding Glucose SAT solver

  • Sébastien Labbé (2023): adding Kissat SAT solver

Classes and Methods#

class sage.sat.solvers.dimacs.DIMACS(command=None, filename=None, verbosity=0, **kwds)[source]#

Bases: 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)[source]#

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. If None then the class variable command is used. (default: None)

  • filename – a filename to write clauses to in DIMACS format, must be writable. If None 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)[source]#

Solve this instance and return the parsed output.

INPUT:

  • assumptions – ignored, accepted for compatibility with other solvers (default: None)

OUTPUT:

  • If this instance is SAT: A tuple of length nvars()+1 where the i-th entry holds an assignment for the i-th variables (the 0-th entry is always None).

  • If this instance is UNSAT: False

EXAMPLES:

When the problem is SAT:

sage: from sage.sat.solvers import RSat
sage: solver = RSat()
sage: solver.add_clause( (1, 2, 3) )
sage: solver.add_clause( (-1,) )
sage: solver.add_clause( (-2,) )
sage: solver()                            # optional - rsat
(None, False, False, True)

>>> from sage.all import *
>>> from sage.sat.solvers import RSat
>>> solver = RSat()
>>> solver.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver.add_clause( (-Integer(1),) )
>>> solver.add_clause( (-Integer(2),) )
>>> solver()                            # optional - rsat
(None, False, False, True)

When the problem is UNSAT:

sage: solver = RSat()
sage: solver.add_clause((1,2))
sage: solver.add_clause((-1,2))
sage: solver.add_clause((1,-2))
sage: solver.add_clause((-1,-2))
sage: solver()                            # optional - rsat
False

>>> from sage.all import *
>>> solver = RSat()
>>> solver.add_clause((Integer(1),Integer(2)))
>>> solver.add_clause((-Integer(1),Integer(2)))
>>> solver.add_clause((Integer(1),-Integer(2)))
>>> solver.add_clause((-Integer(1),-Integer(2)))
>>> solver()                            # optional - rsat
False

With Glucose:

sage: from sage.sat.solvers.dimacs import Glucose
sage: solver = Glucose()
sage: solver.add_clause((1,2))
sage: solver.add_clause((-1,2))
sage: solver.add_clause((1,-2))
sage: solver()                           # optional - glucose
(None, True, True)
sage: solver.add_clause((-1,-2))
sage: solver()                           # optional - glucose
False

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import Glucose
>>> solver = Glucose()
>>> solver.add_clause((Integer(1),Integer(2)))
>>> solver.add_clause((-Integer(1),Integer(2)))
>>> solver.add_clause((Integer(1),-Integer(2)))
>>> solver()                           # optional - glucose
(None, True, True)
>>> solver.add_clause((-Integer(1),-Integer(2)))
>>> solver()                           # optional - glucose
False

With GlucoseSyrup:

sage: from sage.sat.solvers.dimacs import GlucoseSyrup
sage: solver = GlucoseSyrup()
sage: solver.add_clause((1,2))
sage: solver.add_clause((-1,2))
sage: solver.add_clause((1,-2))
sage: solver()                          # optional - glucose
(None, True, True)
sage: solver.add_clause((-1,-2))
sage: solver()                          # optional - glucose
False

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import GlucoseSyrup
>>> solver = GlucoseSyrup()
>>> solver.add_clause((Integer(1),Integer(2)))
>>> solver.add_clause((-Integer(1),Integer(2)))
>>> solver.add_clause((Integer(1),-Integer(2)))
>>> solver()                          # optional - glucose
(None, True, True)
>>> solver.add_clause((-Integer(1),-Integer(2)))
>>> solver()                          # optional - glucose
False
add_clause(lits)[source]#

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.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: ''

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> solver = DIMACS()
>>> solver.var()
1
>>> solver.var(decision=True)
2
>>> solver.add_clause( (Integer(1), -Integer(2) , Integer(3)) )
>>> solver
DIMACS Solver: ''
clauses(filename=None)[source]#

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.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

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS()
>>> solver.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver.clauses()
[((1, 2, 3), False, None)]

>>> solver.add_clause( (Integer(1), Integer(2), -Integer(3)) )
>>> solver.clauses(fn)
>>> print(open(fn).read())
p cnf 3 2
1 2 3 0
1 2 -3 0
<BLANKLINE>
command = ''#
nvars()[source]#

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

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> solver = DIMACS()
>>> solver.var()
1
>>> solver.var(decision=True)
2
>>> solver.nvars()
2
static render_dimacs(clauses, filename, nlits)[source]#

Produce DIMACS file filename from clauses.

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 and rhs.

  • filename – the file to write to

  • nlits -- 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

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS()
>>> solver.add_clause( (Integer(1), Integer(2), -Integer(3)) )
>>> DIMACS.render_dimacs(solver.clauses(), fn, solver.nvars())
>>> print(open(fn).read())
p cnf 3 1
1 2 -3 0
<BLANKLINE>

This is equivalent to:

sage: solver.clauses(fn)
sage: print(open(fn).read())
p cnf 3 1
1 2 -3 0

>>> from sage.all import *
>>> solver.clauses(fn)
>>> print(open(fn).read())
p cnf 3 1
1 2 -3 0
<BLANKLINE>

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

>>> from sage.all import *
>>> DIMACS.render_dimacs([ (Integer(1),Integer(2)), (Integer(1),Integer(2),-Integer(3)) ], fn, Integer(3))
>>> print(open(fn).read())
p cnf 3 2
1 2 0
1 2 -3 0
<BLANKLINE>
var(decision=None)[source]#

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

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> solver = DIMACS()
>>> solver.var()
1
write(filename=None)[source]#

Write DIMACS file.

INPUT:

  • filename – if None 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

>>> from sage.all import *
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> solver.add_clause( (Integer(1), -Integer(2) , Integer(3)) )
>>> _ = solver.write()
>>> for line in open(fn).readlines():
...     print(line)
p cnf 3 1
1 -2 3 0

>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS()
>>> solver.add_clause( (Integer(1), -Integer(2) , Integer(3)) )
>>> _ = solver.write(fn)
>>> 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)[source]#

Bases: 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=0 -model {input}'

>>> from sage.all import *
>>> from sage.sat.solvers import Glucose
>>> solver = Glucose()
>>> solver
DIMACS Solver: 'glucose -verb=0 -model {input}'

When the problem is SAT:

sage: from sage.sat.solvers import Glucose
sage: solver1 = Glucose()
sage: solver1.add_clause( (1, 2, 3) )
sage: solver1.add_clause( (-1,) )
sage: solver1.add_clause( (-2,) )
sage: solver1()                            # optional - glucose
(None, False, False, True)

>>> from sage.all import *
>>> from sage.sat.solvers import Glucose
>>> solver1 = Glucose()
>>> solver1.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver1.add_clause( (-Integer(1),) )
>>> solver1.add_clause( (-Integer(2),) )
>>> solver1()                            # optional - glucose
(None, False, False, True)

When the problem is UNSAT:

sage: solver2 = Glucose()
sage: solver2.add_clause((1,2))
sage: solver2.add_clause((-1,2))
sage: solver2.add_clause((1,-2))
sage: solver2.add_clause((-1,-2))
sage: solver2()                            # optional - glucose
False

>>> from sage.all import *
>>> solver2 = Glucose()
>>> solver2.add_clause((Integer(1),Integer(2)))
>>> solver2.add_clause((-Integer(1),Integer(2)))
>>> solver2.add_clause((Integer(1),-Integer(2)))
>>> solver2.add_clause((-Integer(1),-Integer(2)))
>>> solver2()                            # optional - glucose
False

With one hundred variables:

sage: solver3 = Glucose()
sage: solver3.add_clause( (1, 2, 100) )
sage: solver3.add_clause( (-1,) )
sage: solver3.add_clause( (-2,) )
sage: solver3()                            # optional - glucose
(None, False, False, ..., True)

>>> from sage.all import *
>>> solver3 = Glucose()
>>> solver3.add_clause( (Integer(1), Integer(2), Integer(100)) )
>>> solver3.add_clause( (-Integer(1),) )
>>> solver3.add_clause( (-Integer(2),) )
>>> solver3()                            # optional - glucose
(None, False, False, ..., True)
command = 'glucose -verb=0 -model {input}'#
class sage.sat.solvers.dimacs.GlucoseSyrup(command=None, filename=None, verbosity=0, **kwds)[source]#

Bases: DIMACS

An instance of the Glucose-syrup parallel solver.

For information on Glucose see: http://www.labri.fr/perso/lsimon/glucose/

EXAMPLES:

sage: from sage.sat.solvers import GlucoseSyrup
sage: solver = GlucoseSyrup()
sage: solver
DIMACS Solver: 'glucose-syrup -model -verb=0 {input}'

>>> from sage.all import *
>>> from sage.sat.solvers import GlucoseSyrup
>>> solver = GlucoseSyrup()
>>> solver
DIMACS Solver: 'glucose-syrup -model -verb=0 {input}'

When the problem is SAT:

sage: solver1 = GlucoseSyrup()
sage: solver1.add_clause( (1, 2, 3) )
sage: solver1.add_clause( (-1,) )
sage: solver1.add_clause( (-2,) )
sage: solver1()                            # optional - glucose
(None, False, False, True)

>>> from sage.all import *
>>> solver1 = GlucoseSyrup()
>>> solver1.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver1.add_clause( (-Integer(1),) )
>>> solver1.add_clause( (-Integer(2),) )
>>> solver1()                            # optional - glucose
(None, False, False, True)

When the problem is UNSAT:

sage: solver2 = GlucoseSyrup()
sage: solver2.add_clause((1,2))
sage: solver2.add_clause((-1,2))
sage: solver2.add_clause((1,-2))
sage: solver2.add_clause((-1,-2))
sage: solver2()                            # optional - glucose
False

>>> from sage.all import *
>>> solver2 = GlucoseSyrup()
>>> solver2.add_clause((Integer(1),Integer(2)))
>>> solver2.add_clause((-Integer(1),Integer(2)))
>>> solver2.add_clause((Integer(1),-Integer(2)))
>>> solver2.add_clause((-Integer(1),-Integer(2)))
>>> solver2()                            # optional - glucose
False

With one hundred variables:

sage: solver3 = GlucoseSyrup()
sage: solver3.add_clause( (1, 2, 100) )
sage: solver3.add_clause( (-1,) )
sage: solver3.add_clause( (-2,) )
sage: solver3()                            # optional - glucose
(None, False, False, ..., True)

>>> from sage.all import *
>>> solver3 = GlucoseSyrup()
>>> solver3.add_clause( (Integer(1), Integer(2), Integer(100)) )
>>> solver3.add_clause( (-Integer(1),) )
>>> solver3.add_clause( (-Integer(2),) )
>>> solver3()                            # optional - glucose
(None, False, False, ..., True)
command = 'glucose-syrup -model -verb=0 {input}'#
class sage.sat.solvers.dimacs.Kissat(command=None, filename=None, verbosity=0, **kwds)[source]#

Bases: DIMACS

An instance of the Kissat SAT solver

For information on Kissat see: http://fmv.jku.at/kissat/

EXAMPLES:

sage: from sage.sat.solvers import Kissat
sage: solver = Kissat()
sage: solver
DIMACS Solver: 'kissat -q {input}'

>>> from sage.all import *
>>> from sage.sat.solvers import Kissat
>>> solver = Kissat()
>>> solver
DIMACS Solver: 'kissat -q {input}'

When the problem is SAT:

sage: solver1 = Kissat()
sage: solver1.add_clause( (1, 2, 3) )
sage: solver1.add_clause( (-1,) )
sage: solver1.add_clause( (-2,) )
sage: solver1()                           # optional - kissat
(None, False, False, True)

>>> from sage.all import *
>>> solver1 = Kissat()
>>> solver1.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver1.add_clause( (-Integer(1),) )
>>> solver1.add_clause( (-Integer(2),) )
>>> solver1()                           # optional - kissat
(None, False, False, True)

When the problem is UNSAT:

sage: solver2 = Kissat()
sage: solver2.add_clause((1,2))
sage: solver2.add_clause((-1,2))
sage: solver2.add_clause((1,-2))
sage: solver2.add_clause((-1,-2))
sage: solver2()                           # optional - kissat
False

>>> from sage.all import *
>>> solver2 = Kissat()
>>> solver2.add_clause((Integer(1),Integer(2)))
>>> solver2.add_clause((-Integer(1),Integer(2)))
>>> solver2.add_clause((Integer(1),-Integer(2)))
>>> solver2.add_clause((-Integer(1),-Integer(2)))
>>> solver2()                           # optional - kissat
False

With one hundred variables:

sage: solver3 = Kissat()
sage: solver3.add_clause( (1, 2, 100) )
sage: solver3.add_clause( (-1,) )
sage: solver3.add_clause( (-2,) )
sage: solver3()                           # optional - kissat
(None, False, False, ..., True)

>>> from sage.all import *
>>> solver3 = Kissat()
>>> solver3.add_clause( (Integer(1), Integer(2), Integer(100)) )
>>> solver3.add_clause( (-Integer(1),) )
>>> solver3.add_clause( (-Integer(2),) )
>>> solver3()                           # optional - kissat
(None, False, False, ..., True)
command = 'kissat -q {input}'#
class sage.sat.solvers.dimacs.RSat(command=None, filename=None, verbosity=0, **kwds)[source]#

Bases: DIMACS

An instance of the RSat solver.

For information on RSat see: http://reasoning.cs.ucla.edu/rsat/

EXAMPLES:

sage: from sage.sat.solvers import RSat
sage: solver = RSat()
sage: solver
DIMACS Solver: 'rsat {input} -v -s'

>>> from sage.all import *
>>> from sage.sat.solvers import RSat
>>> solver = RSat()
>>> solver
DIMACS Solver: 'rsat {input} -v -s'

When the problem is SAT:

sage: from sage.sat.solvers import RSat
sage: solver = RSat()
sage: solver.add_clause( (1, 2, 3) )
sage: solver.add_clause( (-1,) )
sage: solver.add_clause( (-2,) )
sage: solver()                            # optional - rsat
(None, False, False, True)

>>> from sage.all import *
>>> from sage.sat.solvers import RSat
>>> solver = RSat()
>>> solver.add_clause( (Integer(1), Integer(2), Integer(3)) )
>>> solver.add_clause( (-Integer(1),) )
>>> solver.add_clause( (-Integer(2),) )
>>> solver()                            # optional - rsat
(None, False, False, True)

When the problem is UNSAT:

sage: solver = RSat()
sage: solver.add_clause((1,2))
sage: solver.add_clause((-1,2))
sage: solver.add_clause((1,-2))
sage: solver.add_clause((-1,-2))
sage: solver()                            # optional - rsat
False

>>> from sage.all import *
>>> solver = RSat()
>>> solver.add_clause((Integer(1),Integer(2)))
>>> solver.add_clause((-Integer(1),Integer(2)))
>>> solver.add_clause((Integer(1),-Integer(2)))
>>> solver.add_clause((-Integer(1),-Integer(2)))
>>> solver()                            # optional - rsat
False
command = 'rsat {input} -v -s'#