Sciweavers

Share
SAT
2015
Springer

SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers

3 years 7 months ago
SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers
In this paper, we present SATGraf, 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. SATGraf has 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...
Zack Newsham, William Lindsay, Vijay Ganesh, Jia H
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where SAT
Authors Zack Newsham, William Lindsay, Vijay Ganesh, Jia Hui Liang, Sebastian Fischmeister, Krzysztof Czarnecki
Comments (0)
books