Exact methods
Solvers with proofs: SAT encodings, integer programming, exact-cover, meet-in-the-middle. Complete methods and what they can actually certify.
Why it's hard
Build a solver
concept
All-different, Régin's matching filter
concept
No-good learning: remembering why you failed
concept
Exact cover and dancing links
concept
Meet in the middle
concept
The tail as its own exact problem
concept
SAT and CSP encodings
concept
LP and ILP relaxations: half a piece everywhere
concept
Iterated maps and divide-and-concur
concept
Quantum approaches: two speedups at their true price
reference
Dead ends