Choco Solver



Portfolio approaches with Choco Solver 4.0


Parallel solving with bound sharing

In Choco Solver, it is possible to make solver portfolios to increase performance.

The main idea is to create several models that are identical from a semantical viewpoint but that have different solving configuration (search heuristics, filtering algorithms, explanations, etc.). Those different models are given to a portfolio that will manage their parallel execution and coordination. In particular, it will inform the solvers anytime a new solution has been found by one of them so that each solver can benefit from the new bound.

We take the example of a grid colouring problem. We compare the runtime of using a single model with two possible search strategies and using a portfolio embedding two models (one for each strategy).

Model:

            
/*
 * Copyright (C) 2017 COSLING S.A.S.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

import org.chocosolver.solver.Model;
import org.chocosolver.solver.ParallelPortfolio;
import org.chocosolver.solver.Solver;
import org.chocosolver.solver.search.strategy.Search;
import org.chocosolver.solver.variables.IntVar;
import org.chocosolver.util.tools.ArrayUtils;

/**
 * Simple example to see how to use parallelism with Choco Solver through portfolios
 * @author Jean-Guillaume FAGES (cosling)
 * @version choco-solver-4.0.4
 */
public class ParallelGridCol {

    private final static int TIME_LIMIT = 30;

    public static void main(String[] args){
        // Grid colouring problem taken from the MiniZinc challenge 2015 at
        // http://www.minizinc.org/challenge2015/mznc2015_probs/grid-colouring/GridColoring.mzn
        // instance parameters
        int n = 10;
        int m = 5;
        System.out.println("%%%%%%%%%%%%%%%%%%%%%%%%%%");
        System.out.println("Solving GridColouring "+n+"_"+m);
        System.out.println("%%%%%%%%%%%%%%%%%%%%%%%%%%");
        System.out.println("Single thread using model search (min domain / min value)");
        solve(n,m,0);
        System.out.println("%%%%%%%%%%%%%%%%%%%%%%%%%%");
        System.out.println("Single thread using Activity Based Search");
        solve(n,m,1);
        System.out.println("%%%%%%%%%%%%%%%%%%%%%%%%%%");
        System.out.println("Portfolio using both model search and Activity Based Search");
        solve(n,m,2);
        System.out.println("%%%%%%%%%%%%%%%%%%%%%%%%%%");
    }

    private static void solve(int n, int m, int conf){
        // solving
        long time = System.currentTimeMillis();
        if (conf<2) { // single thread solving (usual method)
            Model ca = buildModel(n,m,conf==0);
            while (ca.getSolver().solve()){
                System.out.println("Solution found (objective = "+ca.getSolver().getBestSolutionValue()+")");
            }
        }else{ // portfolio optimization (uses bound sharing)
            ParallelPortfolio portfolio = new ParallelPortfolio();
            portfolio.addModel(buildModel(n,m,true));
            portfolio.addModel(buildModel(n,m,false));
            while (portfolio.solve()){
                System.out.println("Solution found (objective = "+portfolio.getBestModel().getSolver().getBestSolutionValue()+")");
            }
        }
        // print solver runtime
        int runtime = (int)((System.currentTimeMillis()-time)/1000);
        if(runtime < TIME_LIMIT) {
            System.out.println("Optimality proved in " + runtime + "s");
        }else{
            System.out.println(TIME_LIMIT+"s timeout reached");
        }
    }

    private static Model buildModel(int n, int m, boolean mznSearch) {
        Model model = new Model("GridColouring "+n+"_"+m);
        // decision variables x[i][j] = k means cell (i,j) takes color k
        IntVar[][] x = model.intVarMatrix("x", n, m, 1, Math.min(n,m));
        // flat representation of x
        IntVar[] vars = ArrayUtils.flatten(x);
        // objective variable
        IntVar objective = model.intVar(1,Math.min(n,m));
        // minimize the objective variable
        model.setObjective(Model.MINIMIZE, objective);

        // objective function : number of colors that are used (colors are symmetrical)
        model.max(objective, vars).post();

        // grid constraints
        for(int i=0;i<n;i++){
            for(int j=i+1;j<n;j++){
                for(int k=0;k<m;k++){
                    for(int l=k+1;l<m;l++){
                        model.or(// at least one of these constraints must be satisfied
                                model.arithm(x[i][k],"!=",x[i][l]),
                                model.arithm(x[i][l],"!=",x[j][l]),
                                model.arithm(x[j][k],"!=",x[j][l]),
                                model.arithm(x[i][k],"!=",x[j][k])
                        ).post();
                    }
                }
            }
        }

        // tuning search strategy
        Solver s = model.getSolver();
        s.limitTime(TIME_LIMIT+"s");
        if(mznSearch) {
            // use search strategy given in the minizinc model (first fail)
            s.setSearch(Search.minDomLBSearch(vars));
        }else{
            // use activity-based search (classical black box search)
            s.setSearch(Search.activityBasedSearch(vars));
        }
        return model;
    }
}
            
        

Output:

            
%%%%%%%%%%%%%%%%%%%%%%%%%%
Solving GridColouring 10_5
%%%%%%%%%%%%%%%%%%%%%%%%%%
Single thread using model search (first fail)
Solution found (objective = 5)
Solution found (objective = 4)
30s timeout reached
%%%%%%%%%%%%%%%%%%%%%%%%%%
Single thread using Activity Based Search
Solution found (objective = 5)
Solution found (objective = 4)
Solution found (objective = 3)
30s timeout reached
%%%%%%%%%%%%%%%%%%%%%%%%%%
Portfolio using both model search and Activity Based Search
Solution found (objective = 5)
Solution found (objective = 4)
Solution found (objective = 3)
Optimality proved in 2s
%%%%%%%%%%%%%%%%%%%%%%%%%%
            
        

A team work

It can be seen that with the first fail heuristic, it is not possible to find the optimal solution in the given time limit. Instead, using Activity Based Search (ABS), a common black-box search strategy, it is possible to find it but not to prove that this solution is optimal. By combining both, one could expect achieving similar performances than ABS that seems better than first fail, plus a slight overhead. However, in practice, the portfolio manages to find the optimum and prove optimality in a couple of seconds. This is much more than each of the above approaches.

How is that possible?

Actually, the two solvers in the portfolio help each other during search. More precisely, ABS is best at FINDING the optimal solution whereas first fail is best at PROVING that no better solution exists. In other words, the two approaches are complementary and form together an efficient approach. In constraint programming as in real life, you better work in team!






Choco Solver Tutorials