CryptoMiniSat Solver

This solver relies on Python bindings provided by upstream cryptominisat.

AUTHORS:

  • Thierry Monteil (2017): complete rewrite, using upstream Python bindings, works with cryptominisat 5.

  • Martin Albrecht (2012): first version, as a cython interface, works with cryptominisat 2.

class sage.sat.solvers.cryptominisat.CryptoMiniSat(verbosity=0, confl_limit=None, threads=None)[source]

Bases: SatSolver

CryptoMiniSat Solver.

INPUT:

  • verbosity – integer between 0 and 15 (default: 0)

  • confl_limit – integer (default: None); abort after this many conflicts. If set to None, never aborts.

  • threads – integer (default: None); the number of thread to use. If set to None, the number of threads used corresponds to the number of cpus.

EXAMPLES:

sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
sage: solver = CryptoMiniSat()                                  # optional - pycryptosat

>>> from sage.all import *
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat
>>> solver = CryptoMiniSat()                                  # optional - pycryptosat
add_clause(lits)[source]

Add a new clause to set of clauses.

INPUT:

  • lits – tuple of nonzero integers

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.cryptominisat import CryptoMiniSat
sage: solver = CryptoMiniSat()                                  # optional - pycryptosat
sage: solver.add_clause((1, -2 , 3))                            # optional - pycryptosat

>>> from sage.all import *
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat
>>> solver = CryptoMiniSat()                                  # optional - pycryptosat
>>> solver.add_clause((Integer(1), -Integer(2) , Integer(3)))                            # optional - pycryptosat
add_xor_clause(lits, rhs=True)[source]

Add a new XOR clause to set of clauses.

INPUT:

  • lits – tuple of positive integers

  • rhs – boolean (default: True); whether this XOR clause should be evaluated to True or False

EXAMPLES:

sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
sage: solver = CryptoMiniSat()                                  # optional - pycryptosat
sage: solver.add_xor_clause((1, 2 , 3), False)                  # optional - pycryptosat

>>> from sage.all import *
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat
>>> solver = CryptoMiniSat()                                  # optional - pycryptosat
>>> solver.add_xor_clause((Integer(1), Integer(2) , Integer(3)), False)                  # optional - pycryptosat
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: # optional - pycryptosat
sage: from sage.sat.solvers import CryptoMiniSat
sage: solver = CryptoMiniSat()
sage: solver.add_clause((1,2,3,4,5,6,7,8,-9))
sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True)
sage: solver.clauses()
[((1, 2, 3, 4, 5, 6, 7, 8, -9), False, None),
((1, 2, 3, 4, 5, 6, 7, 8, 9), True, True)]

>>> from sage.all import *
>>> # optional - pycryptosat
>>> from sage.sat.solvers import CryptoMiniSat
>>> solver = CryptoMiniSat()
>>> solver.add_clause((Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6),Integer(7),Integer(8),-Integer(9)))
>>> solver.add_xor_clause((Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6),Integer(7),Integer(8),Integer(9)), rhs=True)
>>> solver.clauses()
[((1, 2, 3, 4, 5, 6, 7, 8, -9), False, None),
((1, 2, 3, 4, 5, 6, 7, 8, 9), True, True)]

DIMACS format output:

sage: # optional - pycryptosat
sage: from sage.sat.solvers import CryptoMiniSat
sage: solver = CryptoMiniSat()
sage: solver.add_clause((1, 2, 4))
sage: solver.add_clause((1, 2, -4))
sage: fn = tmp_filename()
sage: solver.clauses(fn)
sage: print(open(fn).read())
p cnf 4 2
1 2 4 0
1 2 -4 0

>>> from sage.all import *
>>> # optional - pycryptosat
>>> from sage.sat.solvers import CryptoMiniSat
>>> solver = CryptoMiniSat()
>>> solver.add_clause((Integer(1), Integer(2), Integer(4)))
>>> solver.add_clause((Integer(1), Integer(2), -Integer(4)))
>>> fn = tmp_filename()
>>> solver.clauses(fn)
>>> print(open(fn).read())
p cnf 4 2
1 2 4 0
1 2 -4 0
<BLANKLINE>

Note that in cryptominisat, the DIMACS standard format is augmented with the following extension: having an x in front of a line makes that line an XOR clause:

sage: solver.add_xor_clause((1,2,3), rhs=True)      # optional - pycryptosat
sage: solver.clauses(fn)                            # optional - pycryptosat
sage: print(open(fn).read())                        # optional - pycryptosat
p cnf 4 3
1 2 4 0
1 2 -4 0
x1 2 3 0

>>> from sage.all import *
>>> solver.add_xor_clause((Integer(1),Integer(2),Integer(3)), rhs=True)      # optional - pycryptosat
>>> solver.clauses(fn)                            # optional - pycryptosat
>>> print(open(fn).read())                        # optional - pycryptosat
p cnf 4 3
1 2 4 0
1 2 -4 0
x1 2 3 0
<BLANKLINE>

Note that inverting an xor-clause is equivalent to inverting one of the variables:

sage: solver.add_xor_clause((1,2,5),rhs=False)      # optional - pycryptosat
sage: solver.clauses(fn)                            # optional - pycryptosat
sage: print(open(fn).read())                        # optional - pycryptosat
p cnf 5 4
1 2 4 0
1 2 -4 0
x1 2 3 0
x1 2 -5 0

>>> from sage.all import *
>>> solver.add_xor_clause((Integer(1),Integer(2),Integer(5)),rhs=False)      # optional - pycryptosat
>>> solver.clauses(fn)                            # optional - pycryptosat
>>> print(open(fn).read())                        # optional - pycryptosat
p cnf 5 4
1 2 4 0
1 2 -4 0
x1 2 3 0
x1 2 -5 0
<BLANKLINE>
nvars()[source]

Return the number of variables.

Note that for compatibility with DIMACS convention, the number of variables corresponds to the maximal index of the variables used.

EXAMPLES:

sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
sage: solver = CryptoMiniSat()                                  # optional - pycryptosat
sage: solver.nvars()                                            # optional - pycryptosat
0

>>> from sage.all import *
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat
>>> solver = CryptoMiniSat()                                  # optional - pycryptosat
>>> solver.nvars()                                            # optional - pycryptosat
0

If a variable with intermediate index is not used, it is still considered as a variable:

sage: solver.add_clause((1,-2,4))                               # optional - pycryptosat
sage: solver.nvars()                                            # optional - pycryptosat
4

>>> from sage.all import *
>>> solver.add_clause((Integer(1),-Integer(2),Integer(4)))                               # optional - pycryptosat
>>> solver.nvars()                                            # optional - pycryptosat
4
var(decision=None)[source]

Return a new variable.

INPUT:

  • decision – accepted for compatibility with other solvers; ignored

EXAMPLES:

sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat
sage: solver = CryptoMiniSat()                                  # optional - pycryptosat
sage: solver.var()                                              # optional - pycryptosat
1

sage: solver.add_clause((-1,2,-4))                              # optional - pycryptosat
sage: solver.var()                                              # optional - pycryptosat
5

>>> from sage.all import *
>>> from sage.sat.solvers.cryptominisat import CryptoMiniSat
>>> solver = CryptoMiniSat()                                  # optional - pycryptosat
>>> solver.var()                                              # optional - pycryptosat
1

>>> solver.add_clause((-Integer(1),Integer(2),-Integer(4)))                              # optional - pycryptosat
>>> solver.var()                                              # optional - pycryptosat
5