Reasoning has been a fundamental component of AI since its early ages. However, even very simple mechanisms, based on almost trivial logic are quickly intractable in practice, due to an inherent combinatorial explosion. Despite these strong theoretical limitations, SAT solvers have shown impressive progress over the last 20 years impressive progress, allowing them to routinely solve industrial problems with millions of variables. In this talk, we will review the history of SAT solvers and present how clever encodings of problems, with tight data structures and algorithms have allowed these solvers to defy the theoretical limits of the problems they tackle.