SAT Solving

Readings

References to the Decision Procedures book will noted as DP, while to the Calculus of Computations book will be CC.

• Propositional Logic (PL):
  • CC: 1.1 to 1.4
• Normal forms and decision procedures for PL:
  • CC: 1.6, 1.7
• DPLL and CDCL
  • Slides by Cesare Tinelli
  • Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T)
• SAT solving:
  • DP: Chapter 2
  • Slides by Cesare Tinelli
  • Slides by João Marques-Silva and Mikoláš Janota
  • Slides by Marijn Heule