Complexity Theory of 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:

• Deriving proof complexity lower bounds to demonstrate the hardness of certain formulas for modern solvers;
• Deriving parameterized complexity upper bounds to demonstrate how certain measures of formulas relate to hardness;
• Characterizing SAT/SMT solvers through the lens of machine learning;
• Improving our understanding of encodings and reductions of formulas.

Publications

• Understanding and Improving SAT Solvers via Proof Complexity and Reinforcement Learning
  Chunxiao Li
  PhD thesis (2023)
  [pdf] [bib]

• Limits of CDCL Learning via Merge Resolution
  Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, Vijay Ganesh
  The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
  [pdf] [bib]

• Learning shorter redundant clauses in SDCL using MaxSAT
  Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, Vijay Ganesh
  The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
  [pdf] [bib]

• On the Hierarchical Community Structure of Practical SAT Formulas
  Chunxiao Li, Jonathan Chung, Soham Mukherjee, Marc Vinyals, Noah Fleming, Antonina Kolokolova, Alice Mu, and Vijay Ganesh
  The 24th International Conference on Theory and Applications of Satisfiability Testing (SAT 2021)
  [pdf] [bib]

• Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
  Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, Vijay Ganesh
  The 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020)
  [pdf] [bib] [slides] [talk]

• Understanding and Enhancing CDCL-based SAT Solvers
  Edward Zulkoski
  PhD thesis (2018)
  [pdf] [bib]

• The Proof Complexity of SMT Solvers
  Robert Robere, Antonina Kolkolova, and Vijay Ganesh
  30th International Conference on Computer Aided Verification (CAV 2018)
  [pdf] [bib] [slides]

• Learning-Sensitive Backdoors with Restarts
  Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Liang, Krzysztof Czarnecki and Vijay Ganesh
  24th International Conference on Principles and Practice of Constraint Programming (CP 2018)
  August 27, 2018
  [pdf] [bib]

• The Effect of Structural Measures and Merges on SAT Solver Performance
  Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Jia Liang, Krzysztof Czarnecki and Vijay Ganesh
  24th International Conference on Principles and Practice of Constraint Programming (CP 2018)
  August 27, 2018
  [pdf] [bib]

• Empirically Relating Complexity-theoretic Parameters with SAT Solver Performance
  Edward Zulkoski, Ruben Martins, Christoph M. Wintersteiger, Robert Robere, Jia Liang, Krzysztof Czarnecki and Vijay Ganesh
  Pragmatics of Constraint Reasoning (PoCR 2017)
  August 28, 2017
  [pdf] [bib]