Constraints over integer variables

Overview of constraints based on boolean and integer variables.

Arithmetical constraints

These constraints are used to express arithmetical relationships between two or three variables, or between one or two variables and an integer constant. For instance, a threshold constraint can be posted as following:

model.arithm(x, ">=", 3).post();


Accepted mathematical operators for these constraints are >=, >, <=, <, = and !=. When more than one variable is constrained, one can use the following methods:

String op = ">="; // among ">=", ">", "<=", "<", "=" and "!="
model.arithm(x, op, y).post();
// with x an IntVar and y either an IntVar or an int

String op2 = "+"; // either "+" or "-"
model.arithm(x, op2, y, op, z).post();
// with x and y IntVar, and z is either an int or an IntVar


Other mathematical constraints

Choco-solver also supports other mathematical constraints than arithmetical ones, such as times, div, modulo… In this section, we will consider x, y and z to be IntVar and a and b to be int.

Binary and ternary constraints

times constraints are posted as following:

model.times(x, a, z).post(); // x * a = z
model.times(x, y, a).post(); // x * y = a
model.times(x, y, z).post(); // x * y = z


A div constraint corresponds to a euclidean division. It is posted as following:

model.div(x, y, z).post(); // x / y = z
// it assures that y != 0, and z is rounding towards 0.


modulo constraints are of three types:

model.mod(x, a, b).post(); // x % a = b
model.mod(x, a, z).post(); // x % a = z
model.mod(x, y, z).post(); // x % y = z


An absolute constraint is posted like this:

model.absolute(x, y).post(); // x = |y|


Global constraints

Let min and max be IntVar and let vars be an array of IntVar. One can post the following mathematical constraints to assure that min is the minimum of the variables in vars and max the maximum of them:

model.min(min, vars).post();
model.max(max, vars).post();


Similarly, one can want to sum some variables. For such an operation, one should use the sum constraint:

String op = ">="; // among ">=", ">", "<=", "<", "=" and "!="
model.sum(vars, op, x).post(); // here, it gives sum(vars) >= x


And, finally, for weighted sums, one should use the scalar constraint:

String op = ">="; // among ">=", ">", "<=", "<", "=" and "!="
model.sum(vars, coefs, op, x).post(); // coefs being an array of int
// here, it gives sum(vars[i]*coefs[i]) >= x


Cardinality constraints

allDifferent, allEqual, nvalues, element

Table constraints

Table constraints are really useful and make it possible to encode any relationships. Table constraints expect an array of variables as input and a Tuples object. The latter stores a list of allowed (resp. forbidden) tuples, each of them expresses an allowed (resp. forbidden) combination for the variables.

Consider an ordered set of variables $X=\{X_i \mid i\in I\}$ and an allowed combination $t\in T$, which defined an ordered set of integer values. The ith value in $t$ is denoted $t_i$.

A Table constraint ensures that : $$Table(X,T)\equiv \bigvee_{t \in T}\bigwedge_{i \in I}(X_i = t_i)$$

When dealing with forbidden combinations, the $=$ operator below is replaced by a $\neq$ operator.

Table constraints are also known as constraints in extension since all possible (or impossible) combinations are needed as input.

Table constraints usually provide domain consistency filtering algorithm, with diverse spatial and temporal complexities which depend on the number of variables involved and the number of tuples.

Allowed combinations

Let’s take the example of four variables $X_i = [\![0,3]\!], i \in [1,4]$, that must all be equal. This relationship can be expressed with a Table constraint as follow:

Tuples allEqual = new Tuples(true); // true stands for 'allowed' combinations
model.table(X, allEqual, "CT+").post();


Only defined combinations are solutions.

The parameter "CT+" is optional and defines the filtering algorithm to use. "CT+" is a really good default choice.

Forbidden combinations

Let’s take the previous example but in that case, all variables must not be all be equal. This relationship can be expressed with a Table constraint as follow, with a little difference in the Tuples declaration:

Tuples allEqual = new Tuples(false); // false stands for 'forbidden' combinations
model.table(X, allEqual, "CT+").post();


All undefined combinations are solution, for example {0,0,0,1} or {0,1,2,3}.

Universal value

Under certain conditions, the number of tuples can be reduced by introducing a universal value. Consider $X_i = [\![0,99]\!], i \in [1,3]$, and the following relationship:

1. if $X_1 = 0$ then $X_2 = 0$ and $X_3$ can take any value;
2. else if $X_1 = 3$ then $X_2 = 2$ and $X_3 = 1$.

The allowed tuples are:

{0, 0, 0}
{0, 0, 1}
...
{0, 0, 98}
{0, 0, 99}
{3, 2, 1}


We can see that this relation requires 100 combinations to be expressed and 99 of them are needed to capture $X_3$ can take any value. It’s a use case of universal value.

int STAR = -1;
Tuples rel = new Tuples(true);
rel.setUniversalValue(STAR);
model.table(X, rel).post();


STAR represents the universal value, here $-1$. The value must be taken outside variables domain.

SAT constraints

A SAT solver is embedded in Choco-solver. It is not designed to be accessed directly. The SAT solver is internally managed as a constraint (and a propagator), that’s why it is referred to as SAT constraint in the following.

Clauses can be added with the Model thanks to methods whose name begins with addClause*. There exists two type of clauses declaration: pre-defined ones (such as addClausesBoolLt or addClausesAtMostNMinusOne) or more free ones by specifying a LogOp that represents a clause expression:

model.addClauses(LogOp.and(LogOp.nand(LogOp.nor(a, b), LogOp.or(c, d)), e));
// with static import of LogOp


Automaton-based Constraints

regular, costRegular and multiCostRegular rely on an automaton, declared either implicitly or explicitly. There are two kinds of IAutomaton :

• FiniteAutomaton, needed for regular,
• CostAutomaton, required for costRegular and multiCostRegular.

FiniteAutomaton embeds an Automaton object provided by the dk.brics.automaton library. Such an automaton accepts fixed-size words made of multiple char, but the regular constraints rely on IntVar, so a mapping between char (needed by the underlying library) and int (declared in IntVar) has been made. The mapping enables declaring regular expressions where a symbol is not only a digit between 0 and 9 but any positive number. Then to distinct, in the word 101, the symbols 0, 1, 10 and 101, two additional char are allowed in a regexp: < and > which delimits numbers.

In summary, a valid regexp for the automaton-based constraints is a combination of digits and Java Regexp special characters.

CostAutomaton is an extension of FiniteAutomaton where costs can be declared for each transition.