Lesson 2

The theoretical interest in this problem is explained by its close connections with various areas of computer science. The practical interest comes from the fact that the satisfiability problem provides a convenient language for finding combinatorial objects in practice. For this reason, many practically arising problems are easily formulated in terms of the satisfiability problem: hardware and software verification, resource allocation, scheduling, proof search, and many others.

Moreover, several mathematical conjectures were solved with the help of SAT solvers!