Abstract
The ability of modern SAT solvers to handle huge industrial instances is highly intriguing, if not mysterious. It is well-known that the breakthrough in capacity was enabled by the introduction of the so-called Conflict-Driven-Clause-Learning (CDCL) solvers in the late 90s and early 00s. In the first part of this talk, we review CDCL fundamentals, including the seminal works on the first CDCL solvers GRASP and Chaff, Boolean Constraint Propagation (BCP) algorithm and later works on chronological backtracking. The second part of our talk is about applying SAT to solving optimization problems. Specifically, we review the Polosat algorithm to optimize a user-given black-box function, given a SAT formula. Polosat enabled a breakthrough in the capacity of our industrial tool for cell placement in physical design, and it also serves as an essential component of modern anytime MaxSAT solvers (such as the winner of the latest MaxSAT Evaluation 2022 in all the incomplete categories NuWLS-c).