Modern Constraint Programming, For People Who Know SAT
summary
Overview of modern constraint programming versus SAT with concrete differences: model languages like MiniZinc and Essence, stateful propagators, and lazy clause generation that emits clauses from propagation. Detailed case: the all-different propagator uses bipartite matching and SCCs to achieve generalized arc consistency (no polynomial CNF encoding gives the same), and an incremental implementation speeds propagation by ~168×. Empirical numbers: 9×9 Sudoku times vary (22–57 ms, nodes 1–855), while a 36×36 instance times out in CNF but solves in ~200 ms with 28 recursions. Proof logging via pseudo-Boolean/cutting-planes is proposed.
AI-written summary · about
chapters (26)
- 0:00Intro
- 0:50Modern Constraint Programming
- 2:30Terminology
- 3:38Modelling
- 6:28Reformulation
- 7:05When is CP Actually Good?
- 9:58Variables
- 11:07Constraints
- 13:43Consistency Can Be Hard
- 14:52Do We Care About Consistency?
- 17:27Constraint Propagation is Slow
- 17:43Constraint Propagation is Fast
- 23:22Lazy Clause Generation
- 24:16Two-Colouring a Triangle
- 25:00What Does Propagation Do?
- 25:44Matchings
- 26:32How do Humans Solve Sudoku?
- 29:11Finding Hall Sets?
- 30:52Does GAC Matter?
- 34:51Proof Logging for CP
- 37:33Belief Propagation
- 37:45Parallel Search
- 38:27Competitions
- 38:55Subgraph Isomorphism
- 39:43Colour Ordering
- 42:23Cliques in Random Graphs