What is OR-Tools CP-SAT ?
OR-Tools CP-SAT (Constraint Programming SAT) is a cutting-edge solver developed by Google. It is designed to efficiently handle complex optimization and constraint satisfaction problems. It is used to solve scheduling, resource allocation, and combinatorial optimization challenges.
ORTools enables to model decision problems over finite domains. It provides integer variables, boolean variables and clauses. CPSAT also offers a large set of constraints, including global constraints (alldifferent, sum, circuit, cumulative, regular, table, reservoir, etc.).
CPSAT is an open source library written in C++, with APIs in Java, Python and C#.
An efficient solver mixing technologies
OR-Tools CP-SAT combines differentes approaches : Constraint-Programming (CP), SAT, but also Linear Programming (LP). The CP-SAT hybrids is based on the Lazy Clause Generation (LCG) framework, highlighted by the Chuffed solver. It helps the solver analyse its conflicts while searching for a solution in order to learn from its own mistakes. The Linear Programming integration helps the solver exploiting the objective function in order to converge quickly towards the most promising solutions.
The solver uses a solver Portfolio by default, combining several configurations to accelerate the solving process.
What difference between OR-Tools CP-SAT and Choco Solver ?
Both solvers are excellent and share many features. Nevertheless, we consider CP-SAT to be more effective when using the solver as a black-box. Conversely, Choco Solver is more flexible and facilitates the development and integration of custom components (constraints, heuristics, etc.), allowing to get even better results in many cases. Choosing the best solver therefore depends on the application and its context. We support our clients with both solvers, which we regularly compare using their data.