CppCon 2019 has ended
Back To Schedule
Thursday, September 19 • 16:45 - 17:45
Solve Hard Problems Quickly Using SAT Solvers

Log in to save this to your schedule, view media, leave feedback and see who's attending!

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.

avatar for Martin Hořeňovský

Martin Hořeňovský

Researcher, Locksley.CZ
Martin Hořeňovský is currently a researcher at Locksley.CZ, where he works on converting large master-key systems to SAT. He has taught modern C++ at Czech Technical University in Prague, and maintains Catch2, a popular C++ unit testing framework, in the little free time he has... Read More →

Thursday September 19, 2019 16:45 - 17:45 MDT
Summit 4/5
  • Algorithms/Functional