Abstract
The SAT problem is that of testing the satisfiability of a Boolean formula. It can be described as the simplest of the hard-to-solve problems (technically, NP-complete problems). This difficulty contrasts with the apparent simplicity of the propositional logic on which SAT is based: we only manipulate literals, i.e. variables with values in {true, false} or their negations, and we seek to verify conjunctions of literal disjunctions called clauses. Whether there is such an efficient (polynomial) algorithm for solving SAT is one of the most important problems in theoretical computer science.
SAT marks the frontier of problems for which no algorithm efficient in all cases is known: a translation into SAT is systematically used to show the theoretical impossibility of solving in practice problems of comparable complexity in a wide spectrum of domains. However, over the last few decades, the scientific community has achieved some important victories: many difficult and sometimes very large problems in a variety of fields can be solved in practice once they have been transposed into an equivalent SAT problem. Today, SAT approaches are at the heart of many advances in the world of applications, and in particular in the formal verification of circuits and programs.
