SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers

Title SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers
Author
Abstract

In this paper, we presentSATGraf, a tool for visualizing the evolution of the structure of a Boolean SAT formula in real time as it is being processed by a conflict-driven clause-learning (CDCL) solver. The tool is parametric, allowing the user to define the structure to be visualized. In particular, the tool can visualize the community structure of real-world Boolean satisfiability (SAT) instances and their evolution during solving. Such visualizations have been the inspiration for several hypotheses about the connection between community structure and the running time of CDCL SAT solvers, some which we have already empirically verified.SATGrafhas enabled us in making the following empirical observations regarding CDCL solvers: First, we observe that the Variable State Independent Decaying Sum (VSIDS) branching heuristic consistently chooses variables with a high number of inter-community edges, i.e., high-centrality bridge variables. Second, we observe that the VSIDS branching heuristic and hence the CDCL search procedure is highly focused, i.e., VSIDS disproportionately picks variables from a few communities in the community-structure of input SAT formulas.

Year of Publication
2015
Conference Name
International Conference on Theory and Applications of Satisfiability Testing (SAT)
Date Published
62 - 70
Publisher
Springer
Conference Location
Austin, USA
DOI
10.1007/978-3-319-24318-4_6
Download citation