This talk is divided into two parts of roughly equal length. The first part
introduces the most important techniques of a modern, incremental CDCL
SAT-solver. The second part discusses applications of SAT, and
explains some common techniques one can use when engineering an efficient algorithm
with a SAT-solver as a component.
Niklas finished his Ph.D. on SAT based formal verification in 2005, and has
continued to work as a researcher, first at Cadence Berkeley Labs, and later
at University of California, Berkeley. He is mostly known for co-authoring
the SAT-solver MiniSat, but his interests also include hardware verification and
logic synthesis.
