# Solvers

### Solvers

Numberjack enables you to write a single model in Python which will be encoded for a particular solver. For example, if you are using one of the Mixed Integer Programming (MIP) solvers, then the model will automatically be linearized to a set of linear expressions. For a SAT solver, the model will be encoded to Conjuctive Normal Form (CNF).

- This creates the solver objectsolver = model.load("Mistral")

- This attempts to solve the problem. Returns true if the problem is satisfiable and false otherwise.solver.solve()

- This prints some useful statistics about solving.solver.printStatistics()

- This will set the solver verbosity level to different levels, usually 0, 1 and 2solver.setVerbosity(n)

### Mistral

Mistral is the best supported solver in Numberjack. It supports all the constraints available. It is a state of the art C++ solver. It has added functionality on the normal solver of allowing you to specify the decision variables.

To use Mistral you can:

### SCIP

SCIP is a state of the art open source MIP solver. It can handle a wide range of constraints. It has the extra functionality of being able to handle continuous variables. To create a continuous variable for SCIP to use all you need to do is specify the variable bounds as floats as opposed to integers e.g.

var = Variable(0, 10)

To use SCIP you can:

### MiniSat

MiniSat is an efficient SAT solver which can be used by: