8
$\begingroup$

I am working in an integer optimization problem. All of the decision variables are binary, and the objective is to minimize some cost function. I currently am implementing CBC, but I have been reading that there are some benefits that can come from implementing a CP-SAT solver.

My primary concern is that CP-SAT seems applicable to finding all feasible options, where as CBC is actually geared towards feasible and an objective.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
9
$\begingroup$

CP-SAT is a full fledged (non-mixed) integer programming solver (linear relaxation, presolve, cuts, branching heuristics). It is geared towards optimization, and is actually not very good at enumerating all feasible solution, compared to a tree search based CP solver.

It is also a CP solver, and a damn good one, and a SAT solver.

In our tests, it is on average better than CBC and on par with SCIP on pure integer problems. Still, it misses a few advanced techniques (like tuning how to best use implied bounds in some MIR cuts), and maybe one or two variations on presolve. This translates into CP-SAT being worse that SCIP on a minority of problems, while it is consistently faster on a majority of them).

So the best answer is that you should try. Make sure that you use 8 threads when using CP-SAT for improved performance.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Hi Laurent! Is BOP also recommended in this case (all boolean variables) or is it intended for other kind of problems? I didn't quite find many examples of this particular solver $\endgroup$
    – Stradivari
    Commented May 12, 2020 at 22:01
  • 2
    $\begingroup$ BOP is a decent solver tuned for small easy boolean only problems. It has a very short setup time. It is good at finding good solutions fast. Not so good at proving optimality. $\endgroup$
    – Laurent Perron
    Commented May 12, 2020 at 22:14
  • $\begingroup$ I will have to give CP-SAT a try then. Right now I am running a purely binary/bool problem with about 1 million decision variables. The challenge is that I am actually not to concerned about running until optimality, I just wanted to be able to run for a given period of time (~30 min to 2 hours) to provide a decent feasible solution. The two challenges i hit: 1) CBC just goes through the Primal/Dual during that time and returns no feasible solutions, and then with CP-SAT i need to change the formulation since I leverage several thousand RowConstraints. $\endgroup$
    – S moran
    Commented May 12, 2020 at 23:26
  • 2
    $\begingroup$ @dhasson: CP-SAT uses a portfolio of algorithms. Best diversity, thus robustness and performance is hit for 8 threads. $\endgroup$
    – Laurent Perron
    Commented May 13, 2020 at 7:56
  • 1
    $\begingroup$ There are no publications. You can check the minizinc challenge (minizinc.org/challenge2019/results2019.html as well as the 2018 edition). For the MIPLIB, you can check the site for updates by Frederic Didier (hard to find). $\endgroup$
    – Laurent Perron
    Commented May 13, 2020 at 8:03
7
$\begingroup$

CP solvers can find optimal solutions (given enough time and memory). Essentially, like the "bound" part of branch-and-bound, each time you find a feasible solution you redefine feasibility to include "better than the incumbent".

Whether you would be better off with a MIP approach or a CP approach depends a lot on the specific nature of your problem (and the merits of your respective MIP and CP solvers). CP solvers tend to include special purpose "global constraints", such as "all-different" (no two variables in a group take the same value) or "nonoverlap" (two intervals, such as running times for jobs, do not overlap). In my limited experience, the more your problem contains features that can be modeled by those global constraints, the more likely you are to benefit from switching to CP. With a scheduling problem, I would take a serious look at CP. With a set covering problem, I'm not so sure.

Improve this answer
$\endgroup$
3
  • $\begingroup$ This is all very true, but it does not apply to CP-SAT :-) $\endgroup$
    – Laurent Perron
    Commented May 13, 2020 at 8:30
  • $\begingroup$ I assumed the OP meant CP v. CP-SAT. $\endgroup$
    – prubin ♦
    Commented May 14, 2020 at 15:28
  • $\begingroup$ See my answer below, CP-SAT is both a CP solver (constraints) and a IP solver (linear relaxation, cuts...). So the management of the linear objective, a traditional weak point for CP solver, is a strong point for the CP-SAT solver if the problem is dominantly linear. $\endgroup$
    – Laurent Perron
    Commented May 14, 2020 at 15:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.