Solving Problems Declaratively
summary
Models a Y-pentomino cover as an exact-cover matrix and runs three Java engines from Clojure: Tarantella using dancing links, Rolling Stones on SAT4J, and Loco on Choco. Dancing links finds the 10x10 (20 pieces) and a 15x15 (45 pieces) cover and enumerates all solutions (15x15 in ~10 minutes versus a naive Clojure backtracker still running after 24+ hours). SAT solver finds one solution faster on 15x15 and handles “exactly N” and symmetry constraints; constraint solver enables coloring and optimization but runs slower.
AI-written summary · about
chapters (30)
- 0:00Intro
- 0:39The Puzzle
- 3:15Exact Cover Problem
- 4:02Doubly-Linked List
- 4:54Exact Cover Example (Knuth, 2000)
- 5:07Dancing Links Knuth
- 6:05Implementation
- 7:13Introducing Tarantella
- 8:16Using Tarantella
- 10:24Solving Y Cover with Dancing Links
- 12:07Declarative Model 41: Exact Cover
- 12:49Our Next Model: Boolean Satisfiability
- 14:33Introducing Rolling Stones
- 15:38How do SAT solvers like SAT4j work?
- 15:58Rolling Stones example
- 16:53Encoding constraints on number of true variables
- 18:02Solving Y Cover with Rolling Stones
- 19:18Timing Tests
- 21:05Rotational symmetry
- 21:49Exactly half the pieces have reflective symmetry
- 22:50Declarative Model #2: Boolean Satisfiability
- 23:22Interlude
- 24:33Our Next Model: Constraint Programming
- 25:19Introducing Loco
- 26:13How do constraint programming solvers work?
- 26:37Solving SAT problems in Loco
- 27:20Solving Y Cover in Loco
- 29:49Three-color Y Cover
- 31:47Declarative Model #3: Constraint Programming
- 32:18Conclusion
related talks
10mSATisfying answers to difficult questions!
49mAn Introduction to Constraint Programming
35mA Peek Inside SAT Solvers
43mPost Functional
33mShall We Play A Game?
36mPlaying Go with Clojure
54mUse a Rust SAT Solver to play better pickleball!
44mAutomated Scientific Discovery Using Insights from Problem Structure