SAT, the propositional satisfiability problem, was the first problem to be shown NP-complete, making it the embodiment of theoretical worst-case complexity. However, SAT has emerged as a central problem for efficiently solving computational problems, from hardware and software verification to planning, combinatorial design, and software dependency. Advances in SAT solving technology since a breakthrough around the millennium have catapulted practical SAT solving ahead by orders of magnitudes, making it a primary tool to solve hard computational problems. The article sheds light on the continuing progress of practical SAT solving through a series of evolutionary innovations and improvements, divided into three eras: pre-revolution, revolution, and evolution.
https://cacm.acm.org/magazines/2023/6/273222-the-silent-revolution-of-sat/fulltext