Abstract
In Boolean calculus, there are three main problems: the encoding of Boolean functions, the satisfiability of a formula for at least one set of variable values, called the SAT problem, and its validity for all variable values, equivalent to the unsatisfiability of its negation. While the BDDs presented in previous lectures have become the standard for function representation, they are less effective for satisfiability, as they compute too much information: a BDD encodes all the vectors of variable values that make a formula true, whereas only one need be found to guarantee satisfiability. The first SAT algorithms, born in the 1960s, were based either on the elimination of variables by logical resolution of a variable against its opposites, or on the systematic exploration of variable values. These algorithms are fundamentally exponential in the worst cases, and often are in practice. In 1972, Cook characterized the NP-complexity class and showed that SAT is the prototype of the NP-complete problem, which explains why its solution was long considered impossible in practice.
However, since the 2000s, a barrier has been broken: new algorithms have appeared, considerably improving solution finding and combining systematic search and solution. Even if their worst cases remain exponential, these constantly improved algorithms now enable SAT problems to be solved on formulas derived from concrete examples and involving hundreds of thousands or even millions of variables, which was quite unthinkable just 15 years ago. They are now widely used in industry, particularly in model checking and test generation for embedded circuits and programs, with a key role in proving the conformance of transformations leading from a high-level circuit specification to integrated electronic components. Regular worldwide competition has played a key role in the development and fine-tuning of these algorithms, which remain largely empirical as we still don't really know why they work so well in practice.
