Advanced Model Checking
Summer Semester 2012
This lecture is about algorithms for SAT and applications of SAT to model checking and related problems.
Version 2012.3 of the slide set is available as amcslides.pdf.
You find a description of the Plaisted-Greenbaum polarity based encoding in our recent TACAS paper.
As background material consider the Handbook of Satisfiability.
SMVFlatten tool to flatten SMV models.