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)

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