Empirically Relating Complexity-theoretic Parameters with SAT Solver Performance

TitleEmpirically Relating Complexity-theoretic Parameters with SAT Solver Performance
Publication TypeConference Paper
Year of Publication2017
AuthorsZulkoski, E., R. Martins, C. Wintersteiger, R. Robere, J. Hui Liang, K. Czarnecki, and V. Ganesh
Conference NamePragmatics of Constraint Reasoning
Date Published08/2017
PublisherEPIC
Abstract

Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as backdoors, treewidth, backbones, and community structure. We first show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Further, we show how some of these parameters can be used as a “lens” to better understand the effects of different solving heuristics. We experiment over three branching heuristics and three restart policies, and demonstrate their effect on solver performance.

Refereed DesignationRefereed

WISE Lab logo

Opportunities

We are looking for postdocs and graduate students interested in working on all aspects of autonomous driving.

For more information, visit Open positions.