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 \(2021\). The lecture notes and slides for other rounds are given elsewhere, please see the MyCourses and the A+ pages of the course.

These notes can only give an introduction to propositional satisfiability. An interested reader can take a look at the following for further information:

• The SAT association tutorials

• Talks of Armin Biere, see especially the “Simons Institute for the Theory of Computing” talks in 2021

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