Satisfiability (SAT) problems come up in a surprising number of situations in computer science, from optimization problems to type checking. Being able to identify when a problem can be reduced to an instance of SAT is a useful tool in a programmer’s and researcher’s toolbox. This allows the reuse of libraries and tools written for this class of problems.

In this tutorial participants will learn how to identify SAT problems and how to encode them using the ‘Ersatz Monad’, which is provided by the Haskell ersatz package. The ersatz package is not a SAT solver itself, but provides a DSL for expressing SAT problems and interfacing with external SAT solvers (such as MiniSat).

The concrete examples will be puzzles and games, allowing the attendees to learn how to spot SAT instances using simple and fun examples, without having to learn and internalize large, complex, examples (such as airline route rules). As we progress through the examples we will relate the puzzles to more ‘real-world’ problems that can be solved with the same methods.

While the tutorial will demonstrate these concepts in Haskell using ersatz, the knowledge is easily transferable to other libraries for encoding SAT instances.