Centrality-Based Improvements to CDCL Heuristics
Authors: Sima Jamali and David Mitchell
Paper Information
Title: | Centrality-Based Improvements to CDCL Heuristics |
Authors: | Sima Jamali and David Mitchell |
Proceedings: | SAT Proceedings |
Editors: | Christoph M. Wintersteiger and Olaf Beyersdorff |
Keywords: | SAT Solver, CDCL, Centrality, Betweenness Centrality |
Abstract: | ABSTRACT. There are many reasons to think that SAT solvers should be able to exploit formula structure, but no standard techniques in modern CDCL solvers make explicit use of structure. We describe modifications to modern decision and clause-deletion heuristics that exploit formula structure by using variable centrality. We show that these improve the performance of Maple LCM Dist, the winning solver from Main Track of the 2017 SAT Solver competition. In particular, using centrality in clause deletion results in solving 9 more formulas from the 2017 Main Track. We also look at a number of measures of solver performance and learned clause quality, to see how the changes affect solver execution. |
Pages: | 10 |
Talk: | Jul 09 17:30 (Session 51F: CDCL) |
Paper: |