Propositional satisfiability and SAT solvers

These are the lecture notes for the first rounds in the Aalto University course CS-E3220 Declarative Programming organized in Autumn \(2020\). The lecture notes and slides for other rounds are given elsewhere, please see the MyCourses page of the course.

Contents:

• Overview
• Propositional formulas: syntax and semantics
  • Syntax
  • Semantics
  • Satisfiability and validity
  • Logical consequences and equivalence
• CNF — The Conjunctive Normal Form
• Solving problems with CNF SAT solvers: The Sudoku example
  • Encoding Sudoku in CNF
  • The DIMACS CNF file format
  • SAT Solver APIs
• Truth tables
• CNF Translations
  • Method 1: Applying local rewriting rules
  • Method 2: Deriving CNF from truth tables
  • Method 3: The Tseitin-translation
• DNF — The Disjunctive Normal Form
• SAT Solvers for CNF Formulas: common preliminaries
  • Partial truth assignments
  • Unit clause propagation
• The DPLL backtracking search procedure
  • Incorporating unit clause propagation
• Conflict-driven clause learning (CDCL) SAT solvers
  • Trails
  • Implication graphs, learned clauses and backjumping
  • Some omitted (major!) components
• Preprocessing
  • Pure literal elimination
  • Blocked clause elimination
• The resolution proof system
• References

Some external links

• The SAT association tutorials

Indices and tables

• Index

• Module Index

• Search Page