Solving SAT and related problems

I am Norbert Manthey, a software engineer and interested in low level programming in C++ or C. I currently work for Amazon AWS and hack constraint solvers in my spare time. I prefer small incremental implementation and prototypes for fast development, but am also familiar with static code analysis tools, typical defects and how to fix and avoid them. I typically perform manual steps exactly once, and then script and automate for future iterations.

I did my PhD in the area of automated reasoning. During studies, I started with using SAT solvers to solve logic puzzles. Next, I started to implement the SAT solver Riss, and performed its resource utilization to propose improvements. I extended this solver further during my PhD, and added formula simplification techniques, parallel solving and model counting techniques.

I started to use Riss as a backend for other tools that rely on SAT, including SAT optimization solvers (MaxSAT), minimum unsatisfiability solvers (MUS) that find a minimal unsatisfiable subformula. As a testbed for incremental solving, I implemented the hardware model checker ShiftBMC. Furthermore, Riss implements the generic incremental SAT solving interface. Hence, Riss can be used as a backend in the software model checker CBMC as well. Most recently, I added Riss as the SAT backend for the SMT solver STP.

My PhD thesis covers SAT from an abstract overview over language details, how to encode real world problems, sequential search and simplification techniques, most of which is illustrated with examples or performance evaluations. I also contains an overview of the work on parallel SAT systems, as well as my own research. Using SAT as a backend in other systems is not part of the thesis -- as it's already a quite long read. In case you want to have a look, this is my PhD thesis.

I now work in software security, and occasionally come back to improve Riss, or related tools. Furthermore, I still participate in annual competitions. I collect the reasoning systems I developped on github.