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
  • Search

© Copyright 2018-2023, Tommi Junttila.

Built with Sphinx using a theme provided by Read the Docs.