Talk: Solve hard problems quickly using SAT solvers

What do robot motion planning, hardware design and verification, software verification, model checking, cryptanalysis and bioinformatics have in common? All of them often rely on SAT solvers. This talk will show you how to solve your own hard problems quickly, by leveraging the decades of research that went into the performance of modern SAT solvers.

We will take a look at what the boolean satisfiability (SAT) problem means, and what kind of problems can be converted into SAT. We will then go over examples to show how real-world problems are expressed as SAT, starting with simple examples and ending with a real world problem we have been working on the last few years.

We will also cover why SAT solvers should be especially interesting to C++ developers, how to effectively drive a SAT solver using C++, how we can transfer domain-specific knowledge to the solver and which factors correlate with being able to solve problems quickly.