SAT Solving : A Mini Course

The material in this page was used for a 3 day mini Ph.D. course offered at IT-U of Copenhagen. It was originally given during the period of 24 November to 26 November, 2003. You can find the course web site here. I think it a good starting point for learning about SAT solving in general.  Therefore, I put the course material on the web and hope it can be of some help to other people. After finishing this course, the students should be more or less up to speed with current research in Boolean Satisfiability solving.

DISCLAIMER: Some of the slides I used were borrowed from other colleagues in the SAT research community, including Sharad Malik, Fadi Aloul, Cong Liu and others. Some of the original authors do not want to put their slides on the web in PowerPoint format. Therefore, I can only put the PDF versions of the slides here. Please do not ask me about the original PowerPoint file. Also, since slides are often copied among researchers, I may not have permission to use some of the slides from the original authors of them.  If you find that I am using some of your slides and you do not want me to do so, please let me know and I will remove the slides in question promptly.

• DAY1: An overview of the Boolean Satisfiability in general. The topics includes the definition of SAT, translating arbitrary Boolean formula into CNF form, the complexity of SAT solving, phase transition phenomenon and basic SAT solving techniques. The slides can be found here.
• DAY2: Efficient implementation of a Davis Logemann Loveland (DLL) Style SAT solver. We discuss efficiency considerations in various aspects of a DLL SAT solver, including decision strategy, BCP mechanism, learning and non-chronological backtracking and other engineering considerations. The slides can be found here. 
• DAY3: Recent developments of SAT solving. In this section, some of the recent advancements in SAT solving related researches are briefly discussed. This is up to date as of November 2003. The topics includes SAT solver validation, unsatisfiable core extraction, incremental SAT solving, pseudo Boolean constraint solver, multi-value SAT solver and Quantified Boolean Formula evaluation. For obvious reasons, I can only cover a small part of the many advancements in SAT research. The slides can be found here. 

Course Project:

    To learn about SAT solving, getting your hands dirty in coding is very important. Therefore, I designed a small SAT solver framework in order to get the students familiar with  SAT solvers. ( I renamed the solvers to PicoSAT to distinguish them from the more famous MiniSAT solver ).

1. The first day's project is to look at the code of picosat_1.cpp, which implements a basic DLL solver without learning. The students were asked to understand it, and try to modify it with decision heuristic DLIS described in DAY2 slides page 24 and better literal counting BCP scheme described in DAY2 slides page 36.
2. The second day's project is to look at the code of picosat_2.cpp, which implements a DLL solver with learning and non-chronological backtracking. The students were asked to compare it with  picosat_1.cpp and see how learning and non-chronological backtracking was implemented. The students were also asked to implement 2 literal watching BCP scheme. Both 2-literal watching and learning are described in DAY2's slides.
3. The students were asked to continue work on picosat_2.cpp and implement VSIDS decision heuristic. VSIDS is also described in DAY2's slides.

If you you have any suggestions/questions, please drop me anemail. My email address is lintaoz at microsoft dot com.