CS-E3220: Propositional satisfiability and SAT solvers
Contents:
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
CS-E3220: Propositional satisfiability and SAT solvers
»
Index
Index