The Boolean Satisfiability problem is historically the first and the most important $NP$-complete problem.
The latter means that any reasonable search problem can be efficiently encoded as an instance of
Satisfiability, and it turns out that in practice this encoding is usually very simple, intuitive and
natural. This has brought about a sizable community of strong researchers with different backgrounds
working on questions centered around the same problem: how to solve Satisfiability practically? The area
has seen quite a remarkable success, including commercial packages, but the mathematical explanation
of how this success is compatible with theoretical NP-completeness of the problem remains
largely missing.
In this talk i will try to give at least a general idea about research in this area, emphasizing its
mathematical component.