Advertisement

The Effect of Structural Measures and Merges on SAT Solver Performance

  • Edward ZulkoskiEmail author
  • Ruben Martins
  • Christoph M. Wintersteiger
  • Jia Hui Liang
  • Krzysztof Czarnecki
  • Vijay Ganesh
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11008)

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.

Keywords

SAT solving Structural measures Merge resolution CDCL 

References

  1. 1.
    The international SAT Competitions web page (2017). http://www.satcompetition.org/
  2. 2.
    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_6CrossRefGoogle Scholar
  3. 3.
    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_8CrossRefGoogle Scholar
  4. 4.
    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_13CrossRefGoogle Scholar
  5. 5.
    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_31CrossRefzbMATHGoogle Scholar
  6. 6.
    Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press (2009)Google Scholar
  7. 7.
    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-9MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Jordi, L.: On the classification of industrial SAT families. In: International Conference of the Catalan Association for Artificial Intelligence, p. 163. IOS Press (2015)Google Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Liang, J.H., Oh, C., Ganesh, V., Czarnecki, K., Poupart, P.: Maple-COMSPS, mapleCOMSPS LRB, maplecomsps CHB. SAT Competition, p. 52 (2016)Google Scholar
  13. 13.
    Mateescu, R.: Treewidth in Industrial SAT Benchmarks (2011). http://research.microsoft.com/pubs/145390/MSR-TR-2011-22.pdf
  14. 14.
    Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic ‘phase transitions’. Nature 400(6740), 133–137 (1999)MathSciNetCrossRefGoogle Scholar
  15. 15.
    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_20CrossRefzbMATHGoogle Scholar
  16. 16.
    Pipatsrisawat, K., Darwiche, A.: A new clause learning scheme for efficient unsatisfiability proofs. In: AAAI Conference on Artificial Intelligence, pp. 1481–1484 (2008)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Robertson, N., Seymour, P.D.: Graph minors. III. Planar tree-width. J Comb Theor Series B 36(1), 49–64 (1984)MathSciNetCrossRefGoogle Scholar
  19. 19.
    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

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Edward Zulkoski
    • 1
    Email author
  • Ruben Martins
    • 2
  • Christoph M. Wintersteiger
    • 3
  • Jia Hui Liang
    • 1
  • Krzysztof Czarnecki
    • 1
  • Vijay Ganesh
    • 1
  1. 1.University of WaterlooWaterlooCanada
  2. 2.Carnegie Mellon UniversityPittsburghUSA
  3. 3.Microsoft ResearchCambridgeUK

Personalised recommendations