The Silent (R)evolution of SAT

What is it about?

Today’s powerful, robust SAT solvers have become primary tools for solving hard computational problems. This article aims to shed light on the continuing progress of practical SAT solving through a series of evolutionary innovations and improvements that have been ongoing since the revolutionary breakthrough around the millennium. Overall, we argue that SAT has earned the title of a silent (r)evolution. We tell the story of SAT divided into three eras: the pre-revolution, the revolution, and the evolution.

Featured Image

Why is it important?

Propositional Satisfiability (SAT) has been a cornerstone of computational complexity theory; now, it has become a central target problem for solving hard computational problems in practice. Since the revolution in SAT solving for decision problems that took place around the millennium, significant efficiency improvements have been achieved, and new methods for certification and trust have been added. Over the last 10 years, SAT further evolved by broadening its applications, including optimization, counting, and even problems involving quantifiers.