FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: