Solving

The following part is the ChocLet version of the Choco tutorial.

Finding one solution

A call to choco.solve() launches a resolution which stops on the first solution found, if any:

// defining model
// ... 

if (choco.solve ()) {
    println (vars); 
} else {
    println ("There is no solution");
}

Enumerate all solution

You can enumerate all solutions of a problem with a simple while loop as follows:

while (choco.solve ()) {
    // do something
}

After the enumeration, the solver closes the search tree and variables are no longer instantiated to a value.

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:

let a = 0 .. 10;
// ...
a.maximize ();

while (choco.solve ()) {
    // An improving solution is found
} 
// The last solution was optimal

In ChocLet a new method named solveOptimal perform the solving loop and restore the variable to the optimal solution.


let a = 0 .. 10;
// ...
a.maximize ();

if (choco.solveOptimal ()) {
// a is the optimal possible value for the problem
    println (a); 
} else {
    println ("There is no valid solution");
}

Search Monitor

ChocLet provide a search monitor onOpenNode, and statistics printing.

choco.onOpenNode (
    fn () {
        // Called on open
    },
    fn () {
        // Called on close
    }
);

choco.printStatistics ();

Search strategy

A search strategy is divided over two functions :

  • Select Var | This function will choose the variable to branch on
  • Select Value | This function will affect a value (present in the var domain) to the selected var

The function strategy allows to define those two functions.


choco.strategy (
    fn (vars) {// Select Var, return the first non instantiated var
        for it in vars {
            if !it.isInstantiated 
                return it; 
        }
    }, 
    fn (val) => val.lower // Select Value, return the lowest value of the var
    // Optional, the list of the vars used during search 
    , vars 
);

Example

import std.choco.globals;

def selectVar (vars) {
    for it in vars {
        if !it.isInstantiated // return the first uninstantiated
            return it;
    }
    return null;
}

def selectValue (var) {
    for it in var {
        if it < 10 return it;
    }
    return var.upper;
}

let vars = [0..2 | i in 0 .. 2];

// define constraints
allDifferent (vars).post ();

choco.strategy (selectVar, selectValue, vars);
while choco.solve () {    
    // We can change the strategy whenever we want
    // of course lambda functions can be used to perform the search
    choco.strategy (
        selectVar,
        fn (var) => var.upper,
        vars
    );

    println (vars);
}