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
--
Zdenek Hanzalek
Industrial Informatics Department,
Czech Institute of Informatics, Robotics and Cybernetics,
Czech Technical University in Prague,
Jugoslavskych partyzanu 1580/3, 160 00 Prague 6, Czech Republic
https://rtime.ciirc.cvut.cz/~hanzalek/
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
