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 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 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 is an efficient SAT solver which can be used by: