The CP-SAT solver
Constraint Programming with Boolean Satisfiability
What is CP-SAT
CP-SAT stands for Constraint Programming with Boolean Satisfiability. It is the flagship solver of the Google OR-Tools suite, designed to solve combinatorial optimisation problems defined over integer variables.
CP-SAT combines two complementary approaches:
- Constraint programming (CP): rules that the solution must satisfy are declared, and the solver searches for valid assignments. The word "programming" here means devising a plan, not writing code
- Boolean satisfiability (SAT): the problem is encoded as logical clauses (true/false). The solver uses advanced SAT techniques (conflict clause learning, unit propagation, restarts)
This combination makes CP-SAT particularly effective for scheduling and assignment problems, where the best combination must be found among millions of possibilities.
How CP-SAT works
The solver operates in three phases that repeat in a loop:
1. Assignment. The solver chooses a variable (for example: "does agent Martin work the 6am-2pm shift on Monday?") and assigns it a value (yes or no).
2. Propagation. Once a variable is fixed, constraints propagate the consequences to all other variables. If Martin works Monday morning, he cannot work Monday afternoon (one shift per day), he cannot work Sunday evening (minimum 11h rest), and Monday morning coverage need is reduced by one. This propagation instantly eliminates millions of impossible combinations.
3. Backtracking. If the solver reaches a dead end (no valid value for a variable), it backtracks to a previous decision and tries another value. SAT techniques allow learning from dead ends to avoid repeating them.
This cycle repeats until the optimal solution is found or the configured time limit is reached.
Variables and constraints
CP-SAT works exclusively with integers. All variables, constraints, and objectives are expressed as integers.
Variable types:
- Boolean (0 or 1): "is agent X assigned to shift Y on day Z?" This is the main type used in scheduling
- Integer (bounded domain): "how many minutes does agent X work this month?"
- Interval (start, duration, end): used for scheduling problems with overlap
Constraint types:
AddExactlyOne(): exactly one shift per day per agentAddAtMostOne(): at most one agent on a given postAddNoOverlap(): no temporal overlap on a resourceOnlyEnforceIf(): conditional constraint ("if the agent is qualified for this function, then they can work this shift")- Linear inequalities: sum of hours ≤ contractual hours
Hard vs soft constraints
CP-SAT distinguishes two types of constraints:
Hard constraints (mandatory). They must be satisfied. If the solver cannot satisfy all of them, it returns INFEASIBLE. Examples in Planopti:
- One shift per day per agent
- Minimum 11-hour rest between two shifts
- An agent can only work shifts matching their qualifications
- Vacations, public holidays, and fixed days are respected
Soft constraints (objectives). They are desirable but not mandatory. Each violation incurs a cost (penalty) that the solver seeks to minimise. Examples in Planopti:
- Shift coverage (penalty per uncovered post)
- Minimum 8 rest days per month (penalty per missing day)
- Guarantee one full weekend off per month (penalty per agent without a weekend)
- Fair distribution of working days within a group
- No more than 6 consecutive working days (penalty per violation)
Objective function
The solver's objective is to minimise the weighted sum of penalties. Each soft constraint has a configurable weight reflecting its priority:
- An uncovered post has a high penalty (10,000 per unit) as it is critical for operations
- A missed guaranteed weekend has a medium penalty (5,000 per agent) as it is important but not blocking
- A fairness gap has a lower penalty (50 per gap) as it is a quality objective
The scheduler can adjust these weights in the solver configuration to reflect their operation's priorities. A lower final score means a better quality schedule.
Resolution statuses
After each run, CP-SAT returns a clear status:
- OPTIMAL: the best possible solution has been found and proven optimal. No other combination can do better
- FEASIBLE: a valid solution has been found, but the solver did not have time to prove it is optimal (time limit reached). The solution is nonetheless usable
- INFEASIBLE: no solution exists that satisfies all hard constraints. This generally means the data is incompatible (too many absences, insufficient qualified agents, unrealistic needs)
- MODEL_INVALID: the mathematical model is incorrectly formulated. Configuration error
The solver also returns statistics: number of conflicts encountered, number of branches explored, resolution time in seconds.
Determinism
CP-SAT is deterministic: the same input data systematically produces the same result. It is not generative AI, not machine learning, not approximate heuristics.
This means:
- No random or unpredictable results
- Reproducible and verifiable results
- No "black box": every solver decision is traceable
- No training data, no statistical model, no bias
Performance
CP-SAT has won the gold medal at the international constraint programming competition (MiniZinc Challenge) every year since 2018.
Performance documented by Google:
- 5 agents, 7 days, 3 shifts: optimal solution in 0.003 seconds
- Industrial problems (hundreds of variables, thousands of constraints): solutions in minutes with a configurable time limit
In Planopti, generating a monthly schedule for a mid-sized company (100 to 150 employees, multiple functional groups, dozens of shift types) takes approximately 2 to 5 minutes. For larger structures (200 to 300+ employees, complex cross-constraints), resolution time can reach 10 to 30 minutes depending on model complexity. The time limit is configurable, and CP-SAT always returns the best solution found within the allotted time.
CP-SAT supports multi-threaded search: several search strategies run in parallel to find the optimal solution faster.
CP-SAT in Planopti
Here is how Planopti concretely uses CP-SAT to generate a monthly schedule:
1. Model construction. Planopti reads dashboard data (staff, qualifications, shifts, needs, constraints, absences) and creates a CP-SAT model with:
- A boolean variable
assign[agent, day, shift]for each possible combination - A boolean variable
is_off[agent, day]for rest days - An integer variable
total_minutes[agent]for tracking hours
2. Constraint injection. Planopti injects hard constraints (qualifications, rest, vacations) and soft constraints (coverage, fairness, weekends) into the model.
3. Resolution. CP-SAT searches for the best possible assignment within the configured time limit (120 seconds by default).
4. Result. Planopti retrieves the solution, translates it into a scheduling grid, and displays it in the dashboard. The scheduler can then make manual adjustments and export.