License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2023.3
URN: urn:nbn:de:0030-drops-190405
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19040/
Perron, Laurent ;
Didier, Frédéric ;
Gay, Steven
The CP-SAT-LP Solver (Invited Talk)
Abstract
The CP-SAT-LP solver is developed by the Operations Research team at Google and is part of the OR-Tools [Laurent Perron and Vincent Furnon, 2023] 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 [Stuckey, 2010]. It draws its inspiration from the chuffed solver [Geoffrey Chu et al., 2023], and from the CP 2013 plenary by Peter Stuckey on Lazy Clause Generation [Stuckey, 2013].
The CP-SAT-LP solver improves upon the chuffed solver [Geoffrey Chu et al., 2023] 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-LP. 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 to integrate tightly the research from the Scheduling on MIP community [Balas, 1985; Applegate and Cook, 1991; Maurice Queyranne, 1993] along with the most advanced scheduling algorithms [Vilím, 2011]. This has enabled breakthroughs in solving and proving hard scheduling instances of the Job-Shop problems [Ding et al., 2019] and Resource Constraint Project Scheduling Problems [Rainer Kolisch and Arno Sprecher, 1997; Artigues et al., 2008].
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 [Luteberget and Sartor, 2023] or Large Neighborhood Search [Paul Shaw, 1998] -, 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-LP 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).
BibTeX - Entry
@InProceedings{perron_et_al:LIPIcs.CP.2023.3,
author = {Perron, Laurent and Didier, Fr\'{e}d\'{e}ric and Gay, Steven},
title = {{The CP-SAT-LP Solver}},
booktitle = {29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
pages = {3:1--3:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-300-3},
ISSN = {1868-8969},
year = {2023},
volume = {280},
editor = {Yap, Roland H. C.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/19040},
URN = {urn:nbn:de:0030-drops-190405},
doi = {10.4230/LIPIcs.CP.2023.3},
annote = {Keywords: Constraint Programming, Operations Research, Sat Solver}
}
|
Keywords: |
|
Constraint Programming, Operations Research, Sat Solver |
|
Collection: |
|
29th International Conference on Principles and Practice of Constraint Programming (CP 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
22.09.2023 |
