SATGraf: Visualizing community structure in boolean SAT instances. : 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.
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Giráldez-Cru, Jesús; Levy, Jordi: Generating SAT instances with community structure (2016)
- Shishmarev, Maxim; Mears, Christopher; Tack, Guido; Garcia de la Banda, Maria: Visual search tree profiling (2016)
- Newsham, Zack; Lindsay, William; Ganesh, Vijay; Liang, Jia Hui; Fischmeister, Sebastian; Czarnecki, Krzysztof: (\mathsfSATGraf): visualizing the evolution of SAT formula structure in solvers (2015)