ABSTRACT

Although this area has a history of over 80 years, it was not until the creation of efficient SAT solvers in the mid-1990s that it became practically important, finding applications in electronic design automation, hardware and software verification, combinatorial optimization, and more. Exploring the theoretical and practical aspects of satisfiabi

chapter 1|10 pages

Sets, lattices, and Boolean algebras

chapter 2|34 pages

Introduction to propositional logic

chapter 3|18 pages

Normal forms of formulas

chapter 4|10 pages

The Craig lemma

chapter 5|20 pages

Complete sets of functors

chapter 6|8 pages

Compactness theorem

chapter 7|32 pages

Clausal logic and resolution

chapter 9|40 pages

Polynomial cases of SAT

chapter 15|4 pages

Conclusions