Dear scheduling researcher,
We are delighted to announce the talk given by Laurent Perron (Google France). The title is "The CP-SAT solver". The seminar will take place on Zoom on Wednesday, March 6 at 14:00 UTC.
Join Zoom Meeting https://cesnet.zoom.us/j/98573827806?pwd=UDRqdzYwbktrR29RQk02MVZqMUtkUT09 Meeting ID: 985 7382 7806 Passcode: 287789 You can follow the seminar online or offline on our Youtube channel as well: https://www.youtube.com/channel/UCUoCNnaAfw5NAntItILFn4A
The abstract follows. The CP-SAT solver is developed by the Operations Research team at Google and is part of the OR-Tools open-source optimization suite. It is an implementation of a purely integral Constraint Programming solver on top of a SAT solver using Lazy Clause Generation. It draws its inspiration from the chuffed solver, and from the CP 2013 plenary by Peter Stuckey on Lazy Clause Generation. The CP-SAT solver improves upon the chuffed solver in two main directions. First, it uses a simplex alongside the SAT engine. Second, it implements and relies upon a portfolio of diverse workers for its search part. The use of the simplex brings the obvious advantages of a linear relaxation on the linear part of the full model. It also started the integration of MIP technology into CP-SAT. This is a huge endeavour, as MIP solvers are mature and complex. It includes presolve -- which was already a part of CP-SAT --, dual reductions, specific branching rules, cuts, reduced cost fixing, and more advanced techniques. It also allows the tight integration of the research from the Scheduling on MIP community along with the most advanced scheduling algorithms. This has enabled breakthroughs in solving and proving hard scheduling instances of the Job-Shop problems and Resource Constraint Project Scheduling Problems. Using a portfolio of different workers makes it easier to try new ideas and to incorporate orthogonal techniques with little complication, except controlling the explosion of potential workers. These workers can be categorized along multiple criteria like finding primal solutions -- either using complete solvers, Local Search or Large Neighborhood Search --, improving dual bounds, trying to reduce the problem with the help of continuous probing. This diversity of behaviors has increased the robustness of the solver, while the continuous sharing of information between workers has produced massive speedups when running multiple workers in parallel. All in all, CP- SAT is a state-of-the-art solver, with unsurpassed performance in the Constraint Programming community, breakthrough results on Scheduling benchmarks (with the closure of many open problems), and competitive results with the best MIP solvers (on purely integral problems).
The next talk in our series will be: Pieter Smet (KU Leuven) | March 20 | Robustness in personnel rostering. For more details, please visit https://schedulingseminar.com/
With kind regards
Zdenek, Mike and Guohua