Boolean Satisfiability Algorithms

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

Course Materials

Homework Assignment


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

fv.txt · Last modified: 2009/06/28 22:13 by ric
Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki