Lauching the resolution process
This file can be downloaded as a jupyter notebook and executed with a Java kernel. The next cell is then used to add the dependency to choco and can be ignored otherwise.
// Add maven dependencies at runtime
%maven org.choco-solver:choco-solver:4.10.13
Finding one solution
A call to solver.solve() launches a resolution which stops on the first solution found, if any:
if(solver.solve()){
// do something, e.g. print out variable values
}else if(solver.hasReachedLimit()){
System.out.println("The solver could not find a solution
nor prove that none exists in the given limits");
}else {
System.out.println("The solver has proved the problem has no solution");
}
If solver.solve() returns true, then a solution has been found and each variable is instantiated to a value.
Otherwise, two cases must be considered:
-
A limit has been declared and reached (
solver.hasReachedLimit()returns true). There may be a solution, but the solver has not been able to find it in the given limit or there is no solution but the solver has not been able to prove it (i.e., to close to search tree) in the given limit. The resolution process stops in no particular place in the search tree. -
No limit has been declared or reached: The problem has no solution and the solver has proved it.
An alternative API exists to search for a first solution and return it.
Solution solution = solver.findSolution();
The behaviour of findSolution() is equivalent to that of solve(): when a solution has been found a Solution is returned. Otherwise, null is returned, indicating that no solution has been found below the given limit (if any).
Enumerating all solutions
You can enumerate all solutions of a problem with a simple while loop as follows:
while(solver.solve()){
// do something, e.g. print out variable values
}
After the enumeration, the solver closes the search tree and variables are no longer instantiated to a value.
An alternative API exists to search for all solutions and return a list of them or an empty list if no solution was found.
List<Solution> solutions = solver.findAllSolutions();
It is also possible to stream solutions:
Stream<Solution> solutionsStream = solver.streamSolutions();
Optimization
In Constraint-Programming, optimization is done by computing improving solutions, until reaching an optimum. Therefore, it can be seen as solving multiple times the model while adding constraints on the fly to prevent the solver from computing dominated solutions.
Mono-objective optimization
The optimization process is the following: anytime a solution is found, the value of the objective variable is stored and a cut is posted. The cut is an additional constraint which states that the next solution must be (strictly) better than the current one. To solve an optimization problem, you must specify which variable to optimize and in which direction:
// to maximize X
model.setObjective(Model.MAXIMIZE, X);
// or model.setObjective(Model.MINIMIZE, X); to minimize X
while(solver.solve()){
// an improving solution has been found
}
// the last solution found was optimal (if search completed)
It also possible to use an alternative API to search for the optimal solution. In that case, there is no need to declare the objective in the model, the paramters can directly be given as input of the methode:
Solution solution = solver.findOptimalSolution(X, Model.MAXIMIZE);
Another API makes possible to find all optimal solutions.
List<Solution> solutions = solver.findAllOptimalSolutions(X, Model.MAXIMIZE);
// alterantively, get a stream of optimal solutions
//Stream<Solution> solutionsStream = solver.streamOptimalSolutions(X, Model.MAXIMIZE);
This is a two-stage method that first searches for an optimal solution, then temporarily fixes the value of the objective and stores all the solutions with this additional constraint in a list.
Adapting the cut
You can use custom cuts by overriding the default cut behavior. The cut computer function defines how the cut should bound the objective variable. The input number is the best solution value found so far, the output number define the new bound. When maximizing (resp. minimizing) a problem, the cut limits the lower bound (resp. upper bound) of the objective variable. For instance, one may want to indicate that the value of the objective variable is the next solution should be greater than or equal to the best value + 10
ObjectiveManager<IntVar, Integer> oman = solver.getObjectiveManager();
oman.setCutComputer(n -> n - 10);
Multi-objective optimization
Pareto
If you have multiple objective to optimize, you have several options. First, you may aggregate them in a function so that you end up with only one objective variable. Second, you can solve the problem multiple times, each one optimizing one variable and possibly fixing some bounds on the other. Third, you can enumerate solutions (without defining any objective) and add constraints on the fly to prevent search from finding dominated solutions. This is done by the ParetoOptimizer object which does the following: Anytime a solution is found, a constraint is posted which states that at least one of the objective variables must be strictly better: Such as $(X_0 < b_0 \lor X_1 < b_1 \lor \ldots \lor X_n < b_n)$ where $X_i$ is the ith objective variable and $b_i$ its value.
Here is a simple example on how to use the findParetoFront(...) API to optimize two variables (a and b):
import org.chocosolver.solver.Model;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.solver.Solver;
import org.chocosolver.solver.Solution;
// simple model
Model model = new Model();
IntVar a = model.intVar("a", 0, 2, false);
IntVar b = model.intVar("b", 0, 2, false);
IntVar c = model.intVar("c", 0, 2, false);
model.arithm(a, "+", b, "=", c).post();
Solver solver = model.getSolver();
// create an object that will store the best solutions and remove dominated ones
List<Solution> front = solver.findParetoFront(new IntVar[]{a,b},Model.MAXIMIZE);
System.out.println("The pareto front has "+front.size()+" solutions : ");
for(Solution s: front){
System.out.println("a = "+s.getIntVal(a)+" and b = "+s.getIntVal(b));
}
The pareto front has 3 solutions :
a = 0 and b = 2
a = 1 and b = 1
a = 2 and b = 0
NOTE: All objectives must be optimized on the same direction (either minimization or maximization).
Lexico
It is also possible to consider several objectives $O_1, 02, …, O_n$ ordered lexicographically. Anytime a solution is found, a constraint is posted which states that the objective variables must be strictly better if the previous ones remain unchanged: $(X_1 < b_1) \lor (X_1 = b_1 \land X_2 < b_2) \lor \ldots \lor( \bigwedge_{1 < i < n} X_i = b_i \land X_n < b_n)$ where $X_i$ is the $i^{th}$ objective variable and $b_i$ its value in the solution.
Solution solution = solver.findLexOptimalSolution(objectives, Model.MAXIMIZE);
Propagation
One may want to propagate all constraints without search for a solution.
This can be achieved by calling solver.propagate().
This method runs, in turn, the domain reduction algorithms of the constraints until it reaches a fix point.
It may throw a ContradictionException if a contradiction occurs.
In that case, the propagation engine must be flushed calling solver.getEngine().flush()
to ensure there is no pending events.
WARNING: If there are still pending events in the propagation engine, the propagation may results in unexpected results.