As our first constraint language, we’ll use propositional satisfiability (SAT). The SAT problem is the first problem proven to be \( \NP \)-complete [Cook1971]. It has been studied intensively during the last decades, in both theory and practice view points. Highly efficient SAT solvers, that can solve many problem instances with hundreds of thousands of variables and millions of constraints, exist. However, due to the nature of NP-complete problems, on some hand-crafted instances with only hundreds of variables, the very same solvers can fail badly, meaning that their running times are so large that they do not terminate in practise.
Propositional formulas, satisfiability
Problem solving with SAT solvers
Truth tables and normal forms
Fundamentals of SAT solvers
Resolution proof system