# 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=None, verbose=0)

Initializes the instance

INPUT:

• `solver` – (default: `None`) Specify a Linear Program (LP) solver to be used. If set to `None`, the default one is used. For more information on LP 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.

EXAMPLES:

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

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