A Peek Inside SAT Solvers
Check out the video on ClojureTV!
The goal of this talk was to introduce SAT solving, learn some cool algorithms, and get everyone excited about declarative programming. Go check core.logic and rule engines as well!
Wikipedia
Basic terminology:
Important Pieces from Propositional Logic:
Random:
Videos
Videos taken from a SAT solving workshop between implementers and theorists:
- Marijn Heule on how CDCL solvers work
- Empirical study of SAT solver features (Features chart slide)
- List of all videos from workshop
Discussion-related and general edification videos:
- Advances in Automated Theorem Proving (Complexity class slide)
- Tim Ewald - Clojure: Programming with Hand Tools
- Superoptimizing LLVM by John Regehr
- Random amazing interview with Will Byrd about logic, prolog, etc
Papers
Summary papers that helped me learn about this stuff:
Papers introducing key techniques:
- Chaff/zChaff introducing VSIDS and Two Watched Literals
- GRASP introducing Clause Learning
- Minimizing learned clauses
- Blocked Clause Elimination (a pre-processing techinque that I didn’t discuss)
Other papers:
- Cube and Conquer (very readable, covers basic SAT terminology, combines look-ahead solvers and CDCL solvers, 2 Tb unsat proof!)
- SAT instance visualization (the visualization I used in my slides)
- More SAT instance visualization
Miscellaneous
Parts directly used in my talk:
- My Stackoverflow question about Declarative Programming
- 2016 SAT Competition
- Sudoku in core.logic gist by David Nolan (and updated)
- Sudoku problem in my talk (is Sudoku copyrightable? I have no idea, so I linked it)
Two more technical slideshows:
- Slideshow from a talk about CryptoMiniSat (a real life look at SAT solver implementation)
- Slideshow of how SMT solvers work
Introduction to Z3 syntax (I used an example from here during the SMT section):
Design
I used Chunk, Raleway, and News Gothic MT for the text and Lucida Console for code samples.
I pulled the color palatte from ColourLovers.
Theme Music
This is only in my head, but the theme music for this talk is “Binky” by Snarky Puppy.