# 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:

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

- Overview
- Propositional formulas: syntax and semantics
- CNF — The Conjunctive Normal Form
- Solving problems with CNF SAT solvers: The Sudoku example
- Truth tables
- CNF Translations
- DNF — The Disjunctive Normal Form
- SAT Solvers for CNF Formulas: common preliminaries
- The DPLL backtracking search procedure
- Conflict-driven clause learning (CDCL) SAT solvers
- Preprocessing
- The resolution proof system
- References