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!


Basic terminology:

Important Pieces from Propositional Logic:



Videos taken from a SAT solving workshop between implementers and theorists:

Discussion-related and general edification videos:


Summary papers that helped me learn about this stuff:

Papers introducing key techniques:

Other papers:


Parts directly used in my talk:

Two more technical slideshows:

Introduction to Z3 syntax (I used an example from here during the SMT section):


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.