User guide
Please see the pdf version for a more up-to-date documentation !Creating the Problem
The central element of a choco program is the Problem object.
Problem myPb = new Problem();
Switching from choco to palm only require to use a specific Problem : a PalmProblem.
Problem myPb = new PalmProblem();
Variables
Actually, Three main kind of variables exist :
- IntVar : It describes discrete domains where values are integers.
- EnumIntVar : It corresponds to enumerated domains and should be used when discrete and quite small domains are needed.
- BoundIntVar : Such domains are represented by their lower and upper bounds (propagation is only perform on the bounds). One can use them when large domains are needed.
- RealVar : It describes continous domain and use intervals to represent values.
- SetVar : It describes discrete set domains where a value of a variable is a set. Set vars are encoded with two classical bounds : the union of the all set of possible values called the envelope and the intersection of all set of possible values called the kernel.
Once the Problem has been created, variables are created through factories available on the Problem instead of the classical java constructor. The use of factories allows to redefine them in a specific Problem (as done for the PalmProblem) and ensures that constraints and variables types will remain compatible. The following example of code show how to create a finite domain variable:
IntVar v1 = myPb.makeEnumIntVar("var1", 1, 10);
v1 is an enumerated variable which is called var1 and has a discrete domain from 1 to 10. It has been created for the problem myPb.
Integer Variables
- makeBoundIntVar(String s, int lb, int ub) : creates a finite domain variable with domain (lb .. ub), with name s.
- makeEnumIntVar(String s, int lb, int ub) : creates a finite domain variable whose domain is approximated by bounds (lb .. ub), with name s.
The state of an IntVar can be accessed through the main following public methods on the IntVar class:
- hasEnumeratedDomain(): checks if the variable is an enumerated or a bound one.
- getInf(): returns the lower bound of the variable.
- getSup(): returns the upper bound of the variable.
- getValue(): returns the value if it is instantiated.
- isInstantiated(): checks if the domain is reduced to a singleton.
- canBeInstantiatedTo(int val): checks if the value val is contained in the domain of the variable.
- getDomainSize(): returns the current size of the domain.
The domain of an IntVar can be modified through the main following public methods: Such operations are subject to the backtrack mechanism.
- setMin(): set the lower bound of the variable.
- setMax(): set the upper bound of the variable.
- setVal(): set the value of the variable.
Set Variables
Set variables are still under development but a bit of api is still available.
- makeSetVar(String name, int l, int u): creates a set domain variable with name s where l correponds to the lower bound of the inital enveloppe and b the upper bound.
The state of a SetVar can be accessed through the main following public methods on the SetVar class:
- isInDomainKernel(int x): checks if a value x is contained in the current kernel.
- isInDomainEnveloppe(int x): checks if a value x is contained in the current envelope.
- getDomain(): returns the domain of the variable as a SetDomain. Iterators on envelope or kernel can than be called.
- GetKernelDomainSize(): returns the size of the kernel.
- GetEnveloppeDomainSize(): returns the size of the kernel.
- GetEnveloppeInf(): returns the first available value of the envelope.
- GetEnveloppeSup(): returns the last available value of the envelope.
- GetKernelInf(): returns the first available value of the kernel.
- GetKernelSup(): returns the last available value of the kernel.
- getValue() : returns a table of integer int[] containing the current domain.
The domain of a SetVar can be modified through the main following public methods(ContradictionException can be thrown in case of an inconsistent change) :
- setValIn(int x): set a value inside the kernel.
- setValOut(int x): set a value outside the kernel.
- setVal(int[] val): set the value of the variable.
Real Variables
Real variables are still under development but can be used to solve toy problems such as small systems of equations.
- makeRealVar(String s, double lb, double ub) : creates a continous domain variable whose domain is considered as an interval [lb,ub], with name s.
- getInf(): returns the lower bound of the variable (a double).
- getSup(): returns the upper bound of the variable (a double).
- isInstantiated(): checks if the domain of a variable is reduced to a canonical interval. A canonical interval indicates that the domain has reached the precision given by the user or the solver.
Constraints
Constraints are represented by dedicated objects organized in a class hierarchy. It encapsulates a filtering algorithm which are called when a propagation step occur or when external events happen on the variables belonging to the constraint, such as value removals or bounds modification.
A constraint is stated to a problem by using the method post available on the Problem object : post(Constraint c). Creating a constraint and adding it to the constraint network can be done using the Problem api. For example, adding a constraint of difference between two variables is simply written as follow:
myPb.post(myPb.neq(vars1, vars2));
Integer constraints
Basic constraints
The constraints available with choco are arithmetic constraints (equality, difference, comparisons and linear combination), user-defined binary constraints (AC4,AC3, ...), boolean operators (or, and, implies, ...).
The simplest constraints are comparisons which are defined over expressions of variables such as linear combinations. The following comparison constraints can be accessed through the Problem API:
- neq(IntExp v1, IntExp v2) : v1 != v2.
- eq(IntExp v1, IntExp v2) : v1 = v2.
- leq(IntExp v1, IntExp v2) : v1 <= v2.
- lt(IntExp v1, IntExp v2) : v1 < v2.
To construct complex expressions of variables, simple operators can be used:
- minus(IntExp exp1, IntExp exp2): exp1 - exp2.
- plus(IntExp exp1, IntExp exp2): exp1 + exp2.
- mult(int coef, IntExp exp): coef * exp.
- scalar(int[] coef, IntVar[] vars): coef[1]*vars[1] + ... + coef[n]*vars[n].
- sum(IntVar[] vars): vars[1] + ... + vars[n].
User-defined constraints
Choco supports the statement of constraints defined by arbitrary relations. It offers the possibility of stating binary constraints with several AC Algorithm and also n-ary constraints with a weaker form of propagation.
Binary constraints
The relation defines feasible or infeasible pairs of values for the two variables involved in the constraint. Relations may be defined by two means:
- Tables : specifying those pairs of value for which the constraints is satisfied/unsatisfied.
- Predicates : specfying the method to be called in order to check whether a pair of value is feasible or not.
One the one hand constraints based on tables of values may become rather memory consuming in case of large domains, although relation tables may be shared by different constraints. On the other hand, predicate constraints require little memory as they do not cache thruth values, but imply some run-time overhead for calling the feasibility test. Table constraints are thus well suited for constraints over small domains; while predicate constraints are well suited for situations with large domains.
The creation of a constraint for a relation can be done through the following Problem API :
- makePairAC(IntVar v1, IntVar v2, ArrayList pairs, boolean feas, int ac).
- makePairAC(IntVar v1, IntVar v2, boolean[][] pairs, boolean feas, int ac).
- relationPairAC(IntVar v1, IntVar v2, BinRelation pairs, int ac).
Parameter feas indicates whether the relation models feasible pairs of values or infeasible one (default is infeasible). Parameters pairs contains the definition of the relation. A list of int[] of size 2 in the first case, a boolean[][] in the second case or as a BinRelation in the last case. Finally parameter ac selects the algorithm for enforcing arc-consistency (default ac = 2001). Supported values for this parameter are :
- 3 for AC3 algorithm (searching from scratch for supports on all values)
- 4 for AC4 algorithm (maintaining a count of supports for each value)
- 2001 for the AC2001 algorithm (maintaining the current support of each value)
The definition of a binary relation based on a predicate can be done by inheriting from the CouplesTest class. Have a look on the following example :
public class MyInequality extends CouplesTest{
public boolean checkCouple(int x, int y) {
return x != y;
}
}
You can then state a constraint as the following :
pb.post(pb.relationPairAC(v1, v2,new MyInequality()));
The complete Problem API allow to easily create binary constraint :
- infeasPairAC(IntVar v1, IntVar v2, ArrayList pairs)
- feasPairAC(IntVar v1, IntVar v2, ArrayList pairs)
- relationPairAC(IntVar v1, IntVar v2, BinRelation binR)
- ...
N-Ary Constraints
The situations for binary constraints is extended to the case of relations involving more than two variables, upto a significant difference from the propagation point of view: The propagation engine maintains arc-consistency for binary constraints throughout the solving process, while for n-ary constraints, it uses a weaker propagation mechanism with a forward checking algorithm.
The API for creating such constraints is the following ones:
- makeTupleFC(IntVar[] vs, ArrayList tuples, boolean feas)
- relationTuple(IntVar[] vs, LargeRelation rela)
Defining a specific n-ary relation without storing the tuples can be done as on the following example :
public class NotAllEqual extends TuplesTest {
public boolean checkTuple(int[] tuple) {
for (int i = 1; i < tuple.length; i++) {
if (tuple[i - 1] != tuple[i]) return true;
}
return false;
}
}
Otherwise, the tuples are given in an ArrayList as int[] table given the compatible/incompatible values. One can then state the constraint to the problem :
pb.post(pb.relationTuple(new IntVar[]{x, y, z}, new NotAllEqual()))
Finally, the structure of the Consistency relations can be seen in more details on the following picture :
Advanced constraints
Choco includes several global constraints. Those constraints allows to filter efficiently some inconsistant values. For instance, if several variables should be affected to different values, using a global constraint can offer some additionnal filtering rules (for instance a should be in [1,4], b in [1,4], c in [3,4] and d in [3,4], then one can deduce that a and b cannot be instantiated to 3 or 4; such rule cannot be infered by simple binary constraints).
Here are described som of those constraints :
- pb.allDifferent(IntVar[] vars) creates a constraint ensuring that all pairs of variable have distinct values (which is useful for some matching problems);
- pb.occurrence(IntVar[] vars, int value, IntVar occurrence) creates a constraint to ensure that occurrence will be instantiated to the number of occurrences of valu ein the list of variables vars; this is a specilisation of the following constraint;
- pb.globalCardinality(IntVar[] vars, int[] low, int[] up) creates a constraint ensuring that the number of occurrences of the value 1 in all the variables vars is between low[0] and up[0], and generallay the number of occurrences of the value i in vars is between low[i-1] and up[i-1].
Some other global constraints can be added to Choco in future releases. One can find all the API and constraints available on the Javadoc API.
Set constraints
Choco supports the statement of constraints among sets accessible on the SetModeler class. The api for SetConstraint is available on the SetModeler as show on the following code example :
pb = new Problem();
SetModeler mod = new SetModeler(pb);
pb.post(mod.eqCard(vars[i],3));
The following set constraints are available :
- member(SetVar sv1, int val): states that the variable sv1 contains value val.
- notMember(SetVar sv1, int val): states that the variable sv1 does not contain value val.
- setDisjoint(SetVar sv1, SetVar sv2): states that sv1 and sv2 are disjoint sets ; e.g. that sv1 and sv2 contain no common values.
- setInter(SetVar sv1, SetVar sv2, SetVar inter): states that the inter set variable is the intersection of set variables sv1 and sv2 ; e.g. states that inter contains exactly those values contained in both sets sv1 and sv2.
- eqCard(SetVar sv, int val): states that the cardinality of the set variable is equal to value val.
- geqCard(SetVar sv, int val): states that the cardinality of the set variable is greater or equal equal than value val.
- leqCard(SetVar sv, int val): states that the cardinality of the set variable is equal than value val.
To deal with integer variables, the following mixed constraint are available :
- member(SetVar sv1, IntVar var).
- notMember(SetVar sv1, IntVar var).
- eqCard(SetVar sv, IntVar iv).
- geqCard(SetVar sv, IntVar iv).
- leqCard(SetVar sv, IntVar iv).
Real constraints
Search and Branching
Search for one or all solutions
When the problem is modelled and created thanks to the API described in previous sections, one may want to solve it ! If only one solution is needed, this is quite easy. The following code solves the problem and display the solution :
if (pb.solve() == Boolean.TRUE) {
for(int i = 0; i < pb.getNbIntVars(); i ++) {
System.out.println(pb.getIntVar(i) + " = " +
pb.getIntVar(i).getValue());
}
}
If one wants several solutions, the incremental solve API can be used : nextSolution searches for another solution in the search tree :
if (pb.solve() == Boolean.TRUE) {
do {
for(int i = 0; i < pb.getNbIntVars(); i ++) {
System.out.println(pb.getIntVar(i) + " = " +
pb.getIntVar(i).getValue());
}
} while(pb.nextSolution() == Boolean.TRUE);
}
Optimization
Optimization is done in Choco according to a variable denoting the objective value. The objective function is then expressed as a constraint over this variable and the rest of the problem. The API concerning optimization proposes to minimize/maximize this objective variable (instead of a call to pb.solve()) :
- minimize(IntVar obj, boolean restart).
- maximize(IntVar obj, boolean restart).
Parameter restart is a boolean indicating whether the solver will restart the search after each solution found or if it will keep backtracking from the leaf of the last solution found.
Look at the following knapsack example where a scalar product over three variables is maximized :
Problem pb = new Problem();
IntVar obj1 = pb.makeEnumIntVar("obj1",0,7);
IntVar obj2 = pb.makeEnumIntVar("obj1",0,5);
IntVar obj3 = pb.makeEnumIntVar("obj1",0,3);
IntVar cost = pb.makeBoundIntVar("cout",0,1000000);
int capacite = 34;
int[] volumes = new int[]{7,5,3};
int[] energie = new int[]{6,4,2};
// capacity constraint
pb.post(pb.leq(pb.scalar(volumes,new IntVar[]{obj1,obj2,obj3}),capacite));
// objective function
pb.post(pb.eq(pb.scalar(energie,new IntVar[]{obj1,obj2,obj3}),cost));
pb.maximize(c,false);
Limiting the search space
Limits may be imposed on the search algorithm to avoid spending too much time in the exploration. The limits are updated and checked each time a new node is created . The API is given on the Solver class:
- setTimeLimit(int timeLimit): stops the search algorithm after timeLimit milliseconds have been spent searching.
- setNodeLimit(int nodeLimit): stops the search algorithm after nodeLimit nodes have been expanded.
For example, to stop the search after 30 seconds :
pb.getSolver().setTimeLimit(30000);
To define your own limits/statitistics, you can create a limit object by extending the AbstractGlobalSearchLimit class. Documentation about the definition of your own limits will come later.
Define your own tree search
The construction of the search tree is done according to a serie of Branching objects (that plays the role of achieving intermediate goals in logic programming). The user may specify the sequence of branching objects to be used to build the search tree. For the moment, choco proposes an AssignVar branching that proceeds in assigning variables to values. More complex branching schemes will come soon.
Variable/value selection for AssignVar branching
Choco provides means of composing search trees by specifying the heuristics used for selecting variables and values on integer variables in case of AssignVar branchings. These primitives are based on the following interfaces :
- IIntVarSelector : Interface for the variable selection
- IValIterator : Interface that provide a way of describing an iteration scheme on the domain of a variable
- IValSelector : Interface for a value selection
Default branching heuristics
The default branching heuristic used by Choco is to choose the variable with current minimum domain size first and to take its values in increasing order. The default branchings currently supported by choco are available in the packages choco.integer.search for integer variables (choco.set.search for set variables). Concrete examples of the previous interfaces are the classes MinDomain, MostConstrained, DomOverDeg, RandomIntVarSelector ...
To change the default branching, you can use the API available on the Solver class as shown on the following example :
pb.getSolver().setVarSelector(new RandomIntVarSelector(pb));
Changing the values enumeration/selection can be done in the same way:
// select the value in increasing order
pb.getSolver().setValIterator(new DecreasingDomain());
// or select a random value
pb.getSolver().setValSelector(new RandomIntValSelector());
How to define it own AssignVar branching
You may extend this small library of branching schemes and heuristics by defining your own concrete classes of IIntVarSelector, IValIterator and IValSelector.
Let's take the example of a static variable ordering :
public class StaticVarOrder implements IIntVarSelector {
/**
* the sequence of variables that need be instantiated
*/
protected IntVar[] vars;
public StaticVarOrder(IntVar[] vars) {
this.vars = vars;
}
public IntVar selectIntVar() {
for (int i = 0; i < vars.length; i++) {
if (!vars[i].isInstantiated()) {
return vars[i];
}
}
return null;
}
}
Notice on this example that you only need to implement the method selectIntVar which belongs to the contract of IIntVarSelector. Once the branching is finisched, it returns null and the next branching (if one exist) is taken by the search algorithm to continue the search, otherwise, the search stops as all variable are instantiated.
How to create its own constraint
The constraint hierarchy
A constraint must respect the interface Constraint to be handled by Choco. As a lot of low level methods (to manage the constraint network using a system of listeners) are included in this interface, an abstract class AbstractConstraint provide an implementation of all listeners.
For integer variables, the easiest way to implement your own constraint is to inherit from one of the following classes :
- AbstractUnIntConstraint, AbstractBinIntConstraint, AbstractTernIntConstraint : A default implementation for constraint stating one, two or three variables.
- AbstractLargeIntConstraint : A default implementation for constraint stating more than 3 variables.
In the same way, SetConstraint can inherit from :
- AbstractUnSetConstraint, AbstractBinSetConstraint, AbstractTernSetConstraint.
- AbstractLargeSetConstraint.
Moreover, Constraints stating on integer and set variables can be written by inheriting from AbstractMixedConstraint.