# Solve SAT problems Integer Linear Programming¶

The class defined here is a `SatSolver` that solves its instance using `MixedIntegerLinearProgram`. Its performance can be expected to be slower than when using `CryptoMiniSat`.

class sage.sat.solvers.sat_lp.SatLP(solver, verbose=None, integrality_tolerance=0)

Initializes the instance

INPUT:

• `solver` – (default: `None`) Specify a Mixed Integer Linear Programming (MILP) solver to be used. If set to `None`, the default one is used. For more information on MILP solvers and which default solver is used, see the method `solve` of the class `MixedIntegerLinearProgram`.

• `verbose` – integer (default: `0`). Sets the level of verbosity of the LP solver. Set to 0 by default, which means quiet.

• `integrality_tolerance` – parameter for use with MILP solvers over an inexact base ring; see `MixedIntegerLinearProgram.get_values()`.

EXAMPLES:

```sage: S=SAT(solver="LP"); S
an ILP-based SAT Solver
```

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: S=SAT(solver="LP"); S
an ILP-based SAT Solver
sage: for u,v in graphs.CycleGraph(6).edges(labels=False):
....:     u,v = u+1,v+1
```
nvars()

Return the number of variables.

EXAMPLES:

```sage: S=SAT(solver="LP"); S
an ILP-based SAT Solver
sage: S.var()
1
sage: S.var()
2
sage: S.nvars()
2
```
var()

Return a new variable.

EXAMPLES:

```sage: S=SAT(solver="LP"); S
an ILP-based SAT Solver
sage: S.var()
1
```