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
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