CppCon 2019

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 to do the heavy lifting.
This talk will show you how to solve your own problems with SAT solvers
and leverage the decades of research that has gone into making modern SAT
solvers fast.

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 my employer has
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.