Instructor: Chung-Yang (Ric) Huang / Design Verification Lab, GIEE, NTU

This lecture covers the algorithms and applications of the Boolean Satisfiability (SAT) problem.

Elementary Switching Circuit and Logic Theories

• Overview of Hardware Verification
• Assertion-Based Verification
• Boolean Satisfiability (SAT) Algorithms
  1. Logic Implication and its Applications
  2. DPLL Decision Procedure
  3. Conflict-Driven Learning and Non-Chronological Backtracking
  4. Decision ordering / Restart
  5. Various learning techniques
• SAT-Based Verification
  1. Bounded and Unbounded Modeling Checking
  2. Interpolation Technique
• Future Research Directions

• SAT Algorithms [slides for print] [slides for display]

• SAT Algorithms [Homework(PDF)] | [Homework(Word)] (Due: 9:00am in class, Wednesday, 07/01/2009)

Introduction to modern SAT solvers

• Lintao Zhang and Sharad Malik. The Quest for Efficient Boolean Satisfiability Solvers, in Proceedings of the 14th International Conference on Computer Aided Verification, pp. 17 – 36, 2002.

Boolean SAT Solvers

• SATO, http://www.cs.uiowa.edu/~hzhang/sato.html
• GRASP, http://www.eecs.umich.edu/~faloul/Tools/satire/Grasp2.exe
• zChaff, http://www.princeton.edu/~chaff/
• BerkMin, http://eigold.tripod.com/BerkMin.html
• CSAT, http://cadlab.ece.ucsb.edu/downloads/CSAT.htm
• miniSAT, http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
• PBS, http://www.eecs.umich.edu/~faloul/Tools/pbs4/
• Pueblo, http://www.eecs.umich.edu/~hsheini/pueblo/