The performance of modern satisfiability solvers has improved exponentially every year, and revolutionised areas from electronic design to program analysis. Modern solvers use the Conflict Driven Clause Learning algorithm to explore and prune the search space. I will show that this algorithm has a natural, lattice-based formulation. This formulation provides insights about how to generalise this algorithm to new problem domains and why it works. A generalisation of this algorithm to floating point arithmetic can prove satisfiability of floating point formulae that is beyond the reach of current technology.
This talk is self-contained. I will provide a brief tutorial on modern SAT algorithms and the lattice-theoretic framework I use.