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:
Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, Vijay Ganesh
The 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020)
Robert Robere, Antonina Kolkolova, and Vijay Ganesh
30th International Conference on Computer Aided Verification (CAV 2018)
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]
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]
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]