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).

  •         solver = model.load("Mistral")
    This creates the solver object
  •         solver.solve()
    This attempts to solve the problem. Returns true if the problem is satisfiable and false otherwise.
  •         solver.printStatistics()
    This prints some useful statistics about solving.
  •         solver.setVerbosity(n)
    This will set the solver verbosity level to different levels, usually 0, 1 and 2


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.

solver = model.load("Mistral", decision_variables)
where decision_variables is a list containing the decision variables.

To use Mistral you can:

solver = model.load("Mistral")


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.0, 10.0) # As opposed to
var = Variable(0, 10)

To use SCIP you can:

solver = model.load("SCIP")


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

solver = model.load("MiniSat")