×

zbMATH — the first resource for mathematics

\(\mathsf {SATGraf}\): visualizing the evolution of SAT formula structure in solvers. (English) Zbl 06512565
Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-24317-7/pbk; 978-3-319-24318-4/pbk). Lecture Notes in Computer Science 9340, 62-70 (2015).
Summary: In this paper, we present \mathsf 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. \mathsf 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.
For the entire collection see [Zbl 1323.68009].

MSC:
68Q25 Analysis of algorithms and problem complexity
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78–92. Springer, Heidelberg (2004) · Zbl 1204.68129 · doi:10.1007/978-3-540-24605-3_7
[2] Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using sat procedures instead of bdds. In: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, pp. 317–320. ACM (1999)
[3] Newsham, Z., Ganesh, V., Fischmeister, S., Audemard, G., Simon, L.: Impact of community structure on SAT solver performance. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 252–268. Springer, Heidelberg (2014) · Zbl 1423.68465 · doi:10.1007/978-3-319-09284-3_20
[4] Ansótegui, C., Giráldez-Cru, J., Levy, J.: The community structure of SAT formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 410–423. Springer, Heidelberg (2012) · Zbl 1273.68331 · doi:10.1007/978-3-642-31612-8_31
[5] Clauset, A., Newman, M.E.J., Moore, C.: Finding community structure in very large networks. Physical Review E 70(6), 066111 (2004) · doi:10.1103/PhysRevE.70.066111
[6] Zhang, W., Pan, G., Wu, Z., Li, S.: Online community detection for large complex networks. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, pp. 1903–1909. AAAI Press (2013)
[7] Newman, M.E.J., Girvan, M.: Finding and evaluating community structure in networks (2003). http://arxiv.org/pdf/cond-mat/0308217.pdf
(last viewed December 2013) · Zbl 1032.91716
[8] Kamada, T., Kawai, S.: A general framework for visualizing abstract objects and relations. ACM Trans. Graph. 10(1), 1–39 (1991) · doi:10.1145/99902.99903
[9] Fruchterman, T.M.J., Reingold, E.M.: Graph drawing by force-directed placement. Software: Practice and Experience 21(11), 1129–1164 (1991)
[10] SAT competition 2013 (2013). http://satcompetition.org/2013/
(last viewed January 2014)
[11] Newsham, Z., Lindsay, W., Liang, J., Ganesh, V., Fischmeister, S., Czarnecki, K.: Satgraf sat formula visualization tool. http://bitbucket.org/znewsham/satgraf · Zbl 06512565
[12] Newsham, Z., Lindsay, W., Liang, J., Ganesh, V., Fischmeister, S., Czarnecki, K.: Satgraf structure source. http://bitbucket.org/znewsham/satlib · Zbl 06512565
[13] Newsham, Z., Lindsay, W., Liang, J., Ganesh, V., Fischmeister, S., Czarnecki, K.: Satgraf visualisation executable. https://bitbucket.org/znewsham/satgraf/downloads/satgraf.zip · Zbl 06512565
[14] Kang, K.C., Cohen, S.G., Hess, J.A., Novak, W.E., Peterson, A.S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report, DTIC Document (1990)
[15] Newsham, Z., Lindsay, W., Liang, J., Ganesh, V., Fischmeister, S., Czarnecki, K.: Satgraf: Results (2014). http://satbench.uwaterloo.ca/satgraf/index
(last viewed January 2015)
[16] Taiwan, T., Wang, H.: Minipure (2013). http://edacc4.informatik.uni-ulm.de/SC13/solver-description-download/134
(last viewed January 2014)
[17] Een, N., Sörensson, N.: Minisat: a SAT solver with conflict-clause minimization. In: SAT 2005 (2005)
[18] Sinz, C., Dieringer, E.-M.: DPvis – a tool to visualize the structure of SAT instances. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 257–268. Springer, Heidelberg (2005) · Zbl 1128.68484 · doi:10.1007/11499107_19
[19] Nicolini, C., Dallachiesa, M.: Graphinsight: An interactive visualization system for graph data exploration. http://www.graphinsight.com
[20] Orbe, E., Areces, C., Infante-López, G.: iSat: structure visualization for SAT problems. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 335–342. Springer, Heidelberg (2012) · Zbl 06046621 · doi:10.1007/978-3-642-28717-6_26
[21] Bilgin, A., Ellson, J., Gansner, E., Smyrna, O., Hu, Y., North, S.: Graphviz - graph visualization software. http://www.graphviz.org/
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.