Description: Understanding the Behaviour of SAT solvers
Conflict-driven clause-learning (CDCL) SAT solvers, as well as satisfiability modulo theories (SMT) solvers, routinely solve formulas with thousands to millions of variables and clauses, despite the satisfiability problem being NP-complete. At the same time, small randomly generated formulas are difficult for the same solvers. The goal of this work is to understand which aspects of modern SAT/SMT solvers, as well as which measures of SAT/SMT formulas, relate best to solving performance.
Our line of work follows along 4 main lines of reasoning:
Understanding and Improving SAT Solvers via Proof Complexity and Reinforcement Learning Chunxiao Li PhD thesis ( 2023 ) [pdf] [bib]