SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers

TitleSATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers
Publication TypeConference Paper
Year of Publication2015
AuthorsNewsham, Z., W. Lindsay, VI. Ganesh, J. Hui Liang, S. Fischmeister, and K. Czarnecki
Conference NameInternational Conference on Theory and Applications of Satisfiability Testing (SAT)
Date Published62 - 70
Conference LocationAustin, USA

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 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.

Refereed DesignationRefereed
Related files: 


Looking for motivated students (undergrads and grads) interested in working on embedded software and systems research. Mail Sebastian Fischmeister for further information.