Abstract
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as treewidth, community structure parameters, and a measure of the number of “mergeable” pairs of input clauses. We first show that while most of these parameters correlate well with certain sub-categories of formulas, only the merge-based parameters seem to correlate well across most classes of industrial instances. To further methodically test this connection, we perform a scaling study of mergeability of randomly-generated formulas and CDCL solver running time. We show that as the number of resolvable merge pairs are scaled up for randomly-generated instances while keeping most properties invariant, unsatisfiable instances show a very strong negative correlation with solver runtime. We further show that there is strong negative correlation between the size of learnt clauses and the number of merges as the number of merge pairs are scaled up. A take-away of our work is that mergeability might be a powerful complexity theoretic parameter with which to explain the unusual efficiency of CDCL SAT solvers.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Note that in the resolution proof system, any resolvent of these clauses (e.g., \((x \vee y \vee \lnot y)\)) is effectively useless since it is tautologically true.
References
The international SAT Competitions web page (2017). http://www.satcompetition.org/
Andrews, P.B.: Resolution with merging. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning, pp. 85–101. Springer, Heidelberg (1968). https://doi.org/10.1007/978-3-642-81955-1_6
Ansótegui, C., Bonet, M.L., Giráldez-Cru, J., Levy, J.: The fractal dimension of SAT formulas. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 107–121. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_8
Ansótegui, C., Bonet, M.L., Levy, J.: On the structure of industrial SAT instances. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 127–141. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_13
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). https://doi.org/10.1007/978-3-642-31612-8_31
Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press (2009)
Dilkina, B., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search. Ann. Math. Artif. Intell. 70(4), 399–431 (2014). https://doi.org/10.1007/s10472-014-9407-9
Giráldez-Cru, J., Levy, J.: Locality in random sat instances. In: Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017) (2017)
Godefroid, P., Levin, M.Y., Molnar, D.A., et al.: Automated whitebox fuzz testing. In: Network and Distributed System Security Symposium, pp. 151–166. Internet Society (2008)
Jordi, L.: On the classification of industrial SAT families. In: International Conference of the Catalan Association for Artificial Intelligence, p. 163. IOS Press (2015)
Kilby, P., Slaney, J., Thiébaux, S., Walsh, T.: Backbones and backdoors in satisfiability. In: AAAI Conference on Artificial Intelligence, pp. 1368–1373. AAAI Press (2005)
Liang, J.H., Oh, C., Ganesh, V., Czarnecki, K., Poupart, P.: Maple-COMSPS, mapleCOMSPS LRB, maplecomsps CHB. SAT Competition, p. 52 (2016)
Mateescu, R.: Treewidth in Industrial SAT Benchmarks (2011). http://research.microsoft.com/pubs/145390/MSR-TR-2011-22.pdf
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic ‘phase transitions’. Nature 400(6740), 133–137 (1999)
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, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_20
Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: AAAI Conference on Artificial Intelligence, pp. 1481–1484 (2008)
Pohl, R., Stricker, V., Pohl, K.: Measuring the structural complexity of feature models. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, pp. 454–464. IEEE Press (2013)
Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J Comb Theor Series B 36(1), 49–64 (1984)
Williams, R., Gomes, C., Selman, B.: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 222–230. Springer, Heidelberg (2003). https://doi.org/10.1.1.128.5725
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Zulkoski, E., Martins, R., Wintersteiger, C.M., Liang, J.H., Czarnecki, K., Ganesh, V. (2018). The Effect of Structural Measures and Merges on SAT Solver Performance. In: Hooker, J. (eds) Principles and Practice of Constraint Programming. CP 2018. Lecture Notes in Computer Science(), vol 11008. Springer, Cham. https://doi.org/10.1007/978-3-319-98334-9_29
Download citation
DOI: https://doi.org/10.1007/978-3-319-98334-9_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98333-2
Online ISBN: 978-3-319-98334-9
eBook Packages: Computer ScienceComputer Science (R0)