Lessons
- 1.
Lesson 1: Constraint Satisfaction: Variables, Domains, and Backtracking
Define CSPs formally; implement backtracking search from scratch; understand arc consistency (AC-3) and constraint propagation as the algorithmic foundation CP-SAT is built on.
csp-fundamentals - 2.
Lesson 2: Boolean Satisfiability and DPLL: The Core Algorithm
Encode CSP constraints as SAT clauses; trace the Davis-Putnam-Logemann-Loveland algorithm — unit propagation, pure-literal elimination, and recursive splitting — by hand on small instances.
sat-and-dpll - 3.
Lesson 3: CDCL: Conflict-Driven Clause Learning
Extend DPLL with conflict analysis: implication graphs, the first-UIP cut, asserting clause derivation, and non-chronological backjumping — the algorithm CP-SAT's Boolean layer actually runs.
cdcl-conflict-driven-clause-learning - 4.
Lesson 4: CP-SAT Data Structures: Trail, Watch Lists, and Clause Database
Read the C++ source (sat/sat_base.h, sat/clause.h) to understand the concrete data structures: the assignment trail with decision levels, two-watched-literal scheme for O(1) unit propagation, and how clauses are stored and garbage-collected.
cp-sat-data-structures - 5.
Lesson 5: The CP-SAT Propagator Registry and Solver Loop
Navigate sat/sat_solver.cc and sat/constraint_programming_propagator.cc: how propagators register, how the solver loop interleaves CDCL with CP propagators, and how domain reductions are encoded as Boolean clauses on the trail.
cp-sat-propagator-architecture - 6.
Lesson 6: Lazy Clause Generation: CP-SAT's Hybrid Core
Understand how CP-SAT lazily generates explanations for CP propagations as SAT clauses — the mechanism that lets it outperform pure CP or pure SAT on scheduling problems — traced through the C++ explanation callbacks.
lazy-clause-generation - 7.
Lesson 7: Optimization in CP-SAT: Objective Functions and the LP Relaxation
Cover how CP-SAT handles optimization (minimize/maximize): objective encoding, LP relaxation cuts injected by the GLPK/Glop interface inside CP-SAT, and how the dual bound drives pruning without exposing a separate MIP solver.
cp-sat-objective-and-lp-relaxation - 8.
Lesson 8: The Python API Layer: Protobuf, CP-SAT Model, and Solver Parameters
Trace a Python CpModel from model construction through Protobuf serialisation, the C++ solve call, and response decoding — understanding what the API hides and what SolverParameters you can tune to change solver behaviour.
cp-sat-python-api-internals
Capstone: Instrument and Extend a CP-SAT Timetabling Solver
Take the existing timetabling script, add a custom solution callback to inspect the trail at each decision, tune solver parameters (linearization level, num_search_workers, hints), and extend the model with a new soft constraint — demonstrating full-stack understanding from Python API down to solver internals.
cp-sat-timetabling-capstone