Note on Satisfiability Based Problem Solving

  1. Introduction.
  2. Propositional Logic.
  3. CNF Formulas and Efficient Transformation to CNF.
  4. Resolution and Backtracking
  5. Linear Time Unit Propagation, Horn-SAT and 2-SAT
  6. The CDCL SAT Algorithm
  7. Applications as SAT (currently just circuits and STRIPS planning)
  8. (Currently there is no Section 8).
  9. First Order Logic.
  10. Axoiomatizing Problems.
  11. Solving by Grounding (very preliminary notes)
  12. Some example problems