# Model and Solve¶

## The Model¶

class Numberjack.Model(*expr)

Model object which stores the variables and constraints. The constraints declarations are trees, whose internal nodes are predicates or constraints and leaves are variables.

Model can be initialized with any number of arguments. Each argument will be treated as an Expression or a list of Expression to be added into the model. If no argument is given the Model will be initially empty. An Expression can be subsequently added using the method add() or the operator ‘+=’.

Can be used to add an expression or a collection of expressions to the model like: model += expression

Parameters: expr – Any number of (or nested lists of) Expression instances.

Add an expresion, or a list/tuple/dict of expressions to the model.

Parameters: expr – Any number of (or nested lists of) Expression instances.
constraints = None

A VarArray: containing the roots of the predicate trees.

The solver is passed as a string, the corresponding module is imported, a Solver object created, initialised, and returned.

Parameters: Raises ImportError: solvername (str) – the name of the solver being loaded. Should be one of the modules in Numberjack.solvers. X (list or VarArray) – the decision variables. encoding (EncodingConfiguration) – An EncodingConfiguration instance defining the default encoding for expressions. if the named solver could not be loaded. an instance of a NBJ_STD_Solver subclass.
set_lower_bound(lb)

For weighted CSPs, sets the initial lower bound.

Parameters: ub (int) – The initial lower bound.
set_upper_bound(ub)

For weighted CSPs, sets the initial upper bound.

Parameters: ub (int) – The initial upper bound.
solve_with(library, encoding=None)

Deprecated since version 1.1: Instead you should use load() first and call solve on that solver object instead.

The solver is passed as a string, the corresponding module is imported, a Solver object created, initialised and called. A Solution object (dictionary: var -> val) is returned, if the Model is unsatisfiable, or the solver fails to solve it, the Solution will be empty (None)

variables = None

A VarArray: containing the leaves of the predicate trees.

## Solving Constructs¶

The following is a list of constructs surrounding the solving process.

class Numberjack.NBJ_STD_Solver(Library, Wrapper, model=None, X=None, FD=False, clause_limit=-1, encoding=None)

Generic solver class which will be subclassed by the solver interfaces. Provides common functionality which will be used in each of the solver interfaces.

Note

The user should not need to instantiate this class, instead Numberjack.Model.load() should be used to return an instance of a subclass. However the following methods can be used on that instance.

deduce(exp=None)

Tell the solver to post the negation of the last decision in the current states.

getBacktracks()

Returns the number of backtracks performed during the last search.

getChecks()

Returns the number of constraint checks. for the last search.

getFailures()

Returns the number of failures encountered during the last search.

getNextSolution()

Search for the next solution

getNodes()

Returns the number of nodes explored during the last search.

getNumConstraints()

Get the number of constraints that have been created in the underlying solver. This figure can be different to the number of constraints that you created in your model. For SAT solvers it will be the number of CNF clauses created by the encoding, for MIP solvers it will be the number of linear expressions created.

getNumVariables()

Get the number of variables that have been created in the underlying solver. This figure can be different to the number of variables that you created in your model. For SAT and MIP solvers, this figure will be the number of Boolean variables which had to be created during the encoding step, including any auxiliary variables.

getOptimalityGap()

Returns the optimality gap from the solver. Valid for MIP solvers only.

Raises UnsupportedSolverFunction:
if called on a non MIP solver.
getOptimum()

Returns the current best solution cost from Toulbar2.

Raises UnsupportedSolverFunction:
if called on a solver other than Toulbar2.
getPropags()

Returns the number of constraint propagations performed during the last search.

getTime()

Returns the CPU time required for the last search.

getWorkMem()

Get the limit of working memory, only used for CPLEX.

get_features()

Compute and return the 36 CPHydra features. The feature set includes 32 static features regarding the contraints, domains, etc, and 4 dynamic features about weights, nodes, propagations computed after a 2 second run of Mistral. Note that these can only be compute when the XCSP instance has been loaded directly by Mistral like in the following example:

model = Model()
features = solver.get_features()


Deprecated since version 1.1: This will be replaced with more extensive and flexible functionality in future releases.

get_solution()

Extract a Solution object from the solver representing the list of assigned values.

Return type: Solution
is_opt()

Returns True if the solver found a solution and proved its optimality, False otherwise.

is_sat()

Returns True if the solver found a solution, False otherwise.

is_unsat()

Returns True if the solver proved unsatisfiability, False otherwise.

Asks the underlying MIP solver to load a GMPL file, possibly with a separate data file.

Parameters: Raises UnsupportedSolverFunction: filename – the path to the file. data – optional path to a data file. if called on a non MIP solver.

Asks the underlying MIP solver to load an LP file, possibly with a separate data file.

Parameters: Raises UnsupportedSolverFunction: filename – the path to the file. epsilon – epsilon if called on a non MIP solver.

Parameters: Raises UnsupportedSolverFunction: filename – the path to the file. extension – the file’s extension. if called on a non MIP solver.

This function only allows you to load an XCSP instance into the Mistral solver. You should use the Numberjack.XCSP module to build a generic Numberjack model from an XCSP instance, which can be loaded with other underlying solvers.

Deprecated since version 1.1: Use Numberjack.XCSP instead.

numNodes()

Deprecated since version 1.1: Use getNodes() intead.

num_vars()

Deprecated since version 1.1: Use getNumVariables() intead.

output_cnf(filename)

Output the CNF representation of a model to a file. The model must have been loaded with a SAT-based solver.

Parameters: Raises UnsupportedSolverFunction: filename (str) – The filename of where to output the CNF file. if called on a non SAT-based solver.
output_lp(filename)

Output the LP representation of a model to a file. The model must have been loaded with a MIP-based solver.

Parameters: Raises UnsupportedSolverFunction: filename (str) – The filename of where to output the LP file. if called on a non MIP-based solver.
output_mps(filename)

Output the MPS representation of a model to a file. The model must have been loaded with a MIP-based solver.

Parameters: Raises UnsupportedSolverFunction: filename (str) – The filename of where to output the MPS file. if called on a non MIP-based solver.
post(exp)

Tell the solver to add a constraint in the current state.

Parameters: exp – should be a unary constraint, for example x == 5.
printStatistics()

Asks the solver to print some basic statistics about its last search.

Deprecated since version 1.1.

propagate()

Tell the solver to reach a fixed point.

Returns: False if an inconsistency is found, True otherwise.
reset(full=False)

Resets the data structure of the solver to the initial state.

Parameters: full (bool) – whether the top-level deduction should be undone too.
save()

Tell the solver to save the current state.

setCmdLineOpt(option, value=None, duplicate=False)

Sets Asks the underlying MIP solver to load a GMPL file, possibly with a separate data file.

Parameters: Raises UnsupportedSolverFunction: filename – the path to the file. data – optional path to a data file. if called on a non MIP solver.
setFailureLimit(cutoff)

Sets a limit on the number of failures encountered before aborting search.

setHeuristic(arg1, arg2='No', arg3=0)

Sets the variable and value heuristics.

Note

Currently only supports setting the heuristics for Mistral solvers but a generic method for all solvers is in the works.

setNodeLimit(cutoff)

Sets a limit on the number of nodes explored before aborting search.

setOptimalityGap(gap)

Sets the target relative optimality gap tolerance.

setOption(func, param=None)

Sets an option in Toulbar2 whose name is passed as the first parameter, and value as a second one.

setRandomSeed(seed)

Sets the initial random seed.

Sets the number of threads a solver should use.

setTimeLimit(cutoff)

Sets a limit on the CPU time before aborting search.

setVerbosity(degree)

Sets the verbosity level of the solver.

setWorkMem(mb)

Set the limit of working memory, only used for CPLEX.

shuffle_cnf(*args, **kwargs)

Shuffle the internal CNF representation before writing it to a file. This renames the variables, shuffles their order in each clause, and shuffles the ordering of the clauses. This currently has no affect on the built-in MiniSat or WalkSat solvers since clauses are added directly via their API when they are generated but can be used with any of the other external file based SAT solvers. This should be called before output_cnf().

Parameters: Raises UnsupportedSolverFunction: seed (int) – The seed for the random number generator. if called on a non SAT-based solver.
solutions()

A generator which will yield True until no other solution exists.

solve()

Calls solve on the underlying solver.

Captures KeyboardInterrupt or SystemExit signals and returns None in this case.

Returns: True if the solver found a satisfiable solution, False otherwise.
solveAndRestart(policy=1, base=64, factor=1.3, decay=0.0, reinit=-1)

Calls solve with restarts on the underlying solver.

Deprecated since version 1.1: Restarting is the default in most underlying solvers, currently only Mistral version 1.55 will not perform restarts unless started with this method. Instead you should use solve() which will use restarts by default in other solvers.

startNewSearch()

Initialise structures for a depth first search.

undo(bj=1)

Tell the solver to restore its state to the one last enqueued by ‘save()’

class Numberjack.Solution(vars)

Class which will extract a list of the solution values for a given list of variables. Solution values are order by the order in which the variables are given in vars. This functionality is equivalent to calling Expression.get_value() on each variable, but it is just wrapped here.

Parameters: vars – a Matrix, VarArray, or list of variables to extract the solution for.

## Running Numberjack¶

Numberjack.input(default)

Read command line arguments from the user. This is useful to establish some default parameters of your model and solving process, and to subsequently allow these to be easily changed by specifying a command line argument.

The default argument allows you to specify the list of allowed options, as well as their default values. Any option given on the command line that is not present in this list will raise an error. Values specified on the command line will be coerced into the same data type as is given for that option in default.

Parameters: default (dict) – a dictionary of the valid options and their default values. a dictionary of the options from default, possibly with updated values from the command line. dict

For example, if launching I can change the default parameters of a model like so:

python numberjackfile.py -solver MiniSat -N 10

# numberjackfile.py
default = {'N': 5, 'solver': 'Mistral', 'tcutoff': 30}
param = input(default)
# param will be a dict {'N': 10, 'solver': 'MiniSat', 'tcutoff': 30}


Deprecated since version 1.1: This function will be renamed or replaced in 2.0 to avoid the naming clash with the builtin input function when imported with *.