How does it work?

Cover Image How

CP-SAT is a versatile portfolio solver, centered around a Lazy Clause Generation (LCG) based Constraint Programming Solver, although it encompasses a broader spectrum of technologies.

In its role as a portfolio solver, CP-SAT concurrently executes a multitude of diverse algorithms and strategies, each possessing unique strengths and weaknesses. These elements operate largely independently but engage in information exchange, sharing progress when better solutions emerge or tighter bounds become available.

While this may initially appear as an inefficient approach due to potential redundancy, it proves highly effective in practice. The rationale behind this lies in the inherent challenge of predicting which algorithm is best suited to solve a given problem (No Free Lunch Theorem). Thus, the pragmatic strategy involves running various approaches in parallel, with the hope that one will effectively address the problem at hand. Note that you can also specify which algorithms should be used if you already know which strategies are promising or futile.

In contrast, Branch and Cut-based Mixed Integer Programming solvers like Gurobi implement a more efficient partitioning of the search space to reduce redundancy. However, they specialize in a particular strategy, which may not always be the optimal choice, although it frequently proves to be so.

CP-SAT employs Branch and Cut techniques, including linear relaxations and cutting planes, as part of its toolkit. Models that can be efficiently addressed by a Mixed Integer Programming (MIP) solver are typically a good match for CP-SAT as well. Nevertheless, CP-SAT's central focus is the implementation of Lazy Clause Generation, harnessing SAT-solvers rather than relying primarily on linear relaxations. As a result, CP-SAT may exhibit somewhat reduced performance when confronted with MIP problems compared to dedicated MIP solvers. However, it gains a distinct advantage when dealing with problems laden with intricate logical constraints.

The concept behind Lazy Clause Generation involves the (incremental) transformation of the problem into a SAT-formula, subsequently employing a SAT-solver to seek a solution (or prove bounds by infeasibility). To mitigate the impracticality of a straightforward conversion, Lazy Clause Generation leverages an abundance of lazy variables and clauses.

Notably, the Cook-Levin Theorem attests that any problem within the realm of NP can be translated into a SAT-formula. Optimization, in theory, could be achieved through a simple binary search. However, this approach, while theoretically sound, lacks efficiency. CP-SAT employs a more refined encoding scheme to tackle optimization problems more effectively.

If you want to understand the inner workings of CP-SAT, you can follow the following learning path:

  1. Learn how to get a feasible solution based on boolean logics with SAT-solvers: Backtracking, DPLL, CDCL, VSIDS, ...
  2. Learn how to get provably optimal solutions via classical Mixed Integer Programming:
  3. Learn the additional concepts of LCG Constraint Programming: Propagation, Lazy Clause Generation, ...
  4. Learn the details of CP-SAT:

If you already have a background in Mixed Integer Programming, you may directly jump into the slides of Combinatorial Optimisation and Constraint Programming. This is a full and detailed course on constraint programming, and will probably take you some time to work through. However, it gives you all the knowledge you need to understand the constraint programming part of CP-SAT.

Originally, I wrote a short introduction into each of the topics, but I decided to remove them as the material I linked to is much better than what I could have written. You can find a backup of the old version here.

What Happens in CP-SAT During Solve?

What exactly happens when you run solver.solve(model)?

  1. Model Loading and Verification:

    • The model is read from its protobuf representation.
    • The model is verified for correctness.

  2. Preprocessing (multiple iterations, controlled by max_presolve_iterations):

    1. Presolve (domain reduction):
    2. Expansion of higher-level constraints:
      • Higher-level constraints are expanded into lower-level constraints, CP-SAT actually can propagate efficiently, but which are less comfortable for you to write. See FlatZinc and Flattening for a similar process.
    3. Detection of equivalent variables and affine relations:
    4. Substitution with canonical representations:
      • Detected affine relations are replaced with canonical representations.
    5. Variable probing:
      • Some variables are tested to determine if they can be fixed or if further equivalences can be identified.

  3. Loading and Relaxation:

    • The preprocessed model is loaded into the underlying solver, and linear relaxations are created.

  4. Solution Search:

    • The solver searches for solutions and bounds until the lower and upper bounds converge or another stopping criterion is met (e.g., time limit).
    • Several full subsolvers, each using a unique strategy, are run across different threads. These strategies may include:
      • More linearized models
      • Aggressive restarts
      • Focus on either the lower or upper bound
    • Each subsolver can theoretically find the optimal solution, but some are faster than others.

  5. First Solution Search and Local Search:

    • Additional "first solution searchers" are launched on remaining threads. These stop once a feasible solution is found.
    • Once a feasible solution is discovered, incomplete subsolvers take over, applying local search heuristics such as Large Neighborhood Search (LNS). These subsolvers attempt to improve the solution by iterating through various strategies via a Round Robin approach.
    • During each LNS iteration:
      1. A copy of the model is made, and a solution is selected from the pool of solutions.
      2. A subset of variables is removed from the solution (the method for choosing this subset varies between strategies). The neighborhood of these variables is then explored for a better solution.
      3. The remaining variables are fixed to their current values in the copied model.
      4. The simplified model is presolved with the fixed variables, which often makes the model much easier to solve.
      5. The simplified model is then solved using a complete strategy, but with a short time limit and on a single thread.
      6. If a new solution is found, it’s added to the pool of solutions.

  6. Solution Transformation:

    • The final solution is transformed back into the original model format, allowing you to query the values of the variables as defined in your original model.

This is taken from this talk and slightly extended.

The use of linear programming techniques

As already mentioned before, CP-SAT also utilizes the (dual) simplex algorithm and linear relaxations. The linear relaxation is implemented as a propagator and potentially executed at every node in the search tree but only at lowest priority. A significant difference to the application of linear relaxations in branch and bound algorithms is that only some pivot iterations are performed (to make it faster). However, as there are likely much deeper search trees and the warm-starts are utilized, the optimal linear relaxation may still be computed, just deeper down the tree (note that for SAT-solving, the search tree is usually traversed DFS). At root level, even cutting planes such as Gomory-Cuts are applied to improve the linear relaxation.

The linear relaxation is used for detecting infeasibility (IPs can actually be more powerful than simple SAT, at least in theory), finding better bounds for the objective and variables, and also for making branching decisions (using the linear relaxation's objective and the reduced costs).

The used Relaxation Induced Neighborhood Search RINS (LNS worker), a very successful heuristic, of course also uses linear programming.

Limitations of CP-SAT

While CP-SAT is undeniably a potent solver, it does possess certain limitations when juxtaposed with alternative techniques:

  1. While proficient, it may not match the speed of a dedicated SAT-solver when tasked with solving SAT-formulas, although its performance remains quite commendable.
  2. Similarly, for classical MIP-problems, CP-SAT may not outpace dedicated MIP-solvers in terms of speed, although it still delivers respectable performance.
  3. Unlike MIP/LP-solvers, CP-SAT lacks support for continuous variables, and the workarounds to incorporate them may not always be highly efficient. In cases where your problem predominantly features continuous variables and linear constraints, opting for an LP-solver is likely to yield significantly improved performance.
  4. CP-SAT does not offer support for lazy constraints or iterative model building, a feature available in MIP/LP-solvers and select SAT-solvers. Consequently, the application of exponential-sized models, which are common and pivotal in Mixed Integer Programming, may be restricted.
  5. CP-SAT is limited to the Simplex algorithm and does not feature interior point methods. This limitation prevents it from employing polynomial time algorithms for certain classes of quadratic constraints, such as Second Order Cone constraints. In contrast, solvers like Gurobi utilize the Barrier algorithm to efficiently tackle these constraints in polynomial time.

CP-SAT might also exhibit inefficiency when confronted with certain constraints, such as modulo constraints. However, it's noteworthy that I am not aware of any alternative solver capable of efficiently addressing these specific constraints. At times, NP-hard problems inherently pose formidable challenges, leaving us with no alternative but to seek more manageable modeling approaches instead of looking for better solvers.

The CP-SAT Primer is authored by Dominik Krupke at TU Braunschweig, Algorithms Division. It is licensed under the CC-BY-4.0 license.

The primer is written for educational purposes and may be incomplete or incorrect in places. If you find this primer helpful, please star the GitHub repository, to let me know with a single click that it has made an impact. As an academic, I also enjoy hearing about how you use CP-SAT to solve real-world problems.