Introduction to Satisfiability Solving with Practical Applications

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.

Foundations of Modern CDCL SAT Solver Implementation

put your abstract here

Niklas Een, University of California, Berkeley, USA

...

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.