CryptoMiniSat Solver

This solver relies on Python bindings provided by upstream cryptominisat.

The cryptominisat package should be installed on your Sage installation.

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)

Bases: sage.sat.solvers.satsolver.SatSolver

CryptoMiniSat Solver.

INPUT:

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

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

  • threads – an 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 - cryptominisat
add_clause(lits)

Add a new clause to set of clauses.

INPUT:

  • lits – a 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 - cryptominisat
sage: solver.add_clause((1, -2 , 3))                            # optional - cryptominisat
add_xor_clause(lits, rhs=True)

Add a new XOR clause to set of clauses.

INPUT:

  • lits – a 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 - cryptominisat
sage: solver.add_xor_clause((1, 2 , 3), False)                  # optional - cryptominisat
clauses(filename=None)

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 import CryptoMiniSat
sage: solver = CryptoMiniSat()                              # optional - cryptominisat
sage: solver.add_clause((1,2,3,4,5,6,7,8,-9))               # optional - cryptominisat
sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True)  # optional - cryptominisat
sage: solver.clauses()                                      # optional - cryptominisat
[((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: from sage.sat.solvers import CryptoMiniSat
sage: solver = CryptoMiniSat()                      # optional - cryptominisat
sage: solver.add_clause((1, 2, 4))                  # optional - cryptominisat
sage: solver.add_clause((1, 2, -4))                 # optional - cryptominisat
sage: fn = tmp_filename()                           # optional - cryptominisat
sage: solver.clauses(fn)                            # optional - cryptominisat
sage: print(open(fn).read())                        # optional - cryptominisat
p cnf 4 2
1 2 4 0
1 2 -4 0

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 - cryptominisat
sage: solver.clauses(fn)                            # optional - cryptominisat
sage: print(open(fn).read())                        # optional - cryptominisat
p cnf 4 3
1 2 4 0
1 2 -4 0
x1 2 3 0

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 - cryptominisat
sage: solver.clauses(fn)                            # optional - cryptominisat
sage: print(open(fn).read())                        # optional - cryptominisat
p cnf 5 4
1 2 4 0
1 2 -4 0
x1 2 3 0
x1 2 -5 0
nvars()

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 - cryptominisat
sage: solver.nvars()                                            # optional - cryptominisat
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 - cryptominisat
sage: solver.nvars()                                            # optional - cryptominisat
4
var(decision=None)

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 - cryptominisat
sage: solver.var()                                              # optional - cryptominisat
1

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