A Personal History of Practical SAT Solving
Talkat 50 Years of Satisfiability: The Centrality of SAT in the Theory of Computing · 2021-02-11..05-13
summary
A personal timeline shows concrete leaps: QSAT solved far more instances in SAT Comp 2020, driven by integrating local search plus target phases into a CDCL core; that jump repeats past five-year surges. Winners since 2013 use inprocessing, earlier gains come from 2005 bounded variable elimination and 2009 LBD-based clause reduction; phase saving with rapid restarts speeds both satisfiable and unsatisfiable cases. Implementations hit 2^28 variable limits and produce checkable proofs.
AI-written summary · about