Albert Oliveras: The Power of SAT: Defying NP-Completeness in the Real World

The SAT problem, determining the satisfiability of a formula in propositional
logic, is known by every computer scientist as the canonical NP-complete
problem. However, its practical side is far less renowned: nowadays, many
industrial problems are solved by encoding them as SAT instances and
subsequently processing them with a SAT solver. Concrete examples include the
formal verification of software and hardware, cryptographic protocols, and the
resolution of open mathematical problems.
In the first part of this talk, we will introduce SAT solvers from a near-
user perspective. We will mention specific areas of application, existing
tools, and their functionalities.
In the second part, we will delve into the algorithmic details of these
tools, as well as specific implementation aspects. We will also explain the
characterization of their power by relating them to well-known proof systems.
Finally, we will conclude by discussing more recent work, such as SDCL or
DIP-based Extended Resolution, where the aim is to extend the reasoning
capabilities of these solvers so that they can simulate more powerful proof
systems.