Advertisement

On the Non-degeneracy of Unsatisfiability Proof Graphs Produced by SAT Solvers

  • Rohan FosséEmail author
  • Laurent SimonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11008)

Abstract

Despite the important effort in developing fast and powerful SAT solvers, many aspects of their behaviors remains largely unexplained. We analyze the properties of learnt clauses derived by a typical Conflict Driven Clause Learning algorithm (CDCL) and study how they are linked to their ancestors, in the dependency graph generated by the resolution steps during conflict analysis and clauses minimizations. We show that all these graphs share a common structure: they are non k-degenerated with surprising large values, which mean they contain a very dense subgraph, the K-Core. We unveil the existence of large K-Cores, even on parallelized SAT solvers with clauses exchanges. We show that the analysis of the K-Core allows a good prediction of which literals will occur in future learnt clauses, until the very end of the computation. Moreover, we show that the analysis of the graph allows to identify a set of learnt clauses that will be necessary for deriving the final contradiction. At last, we demonstrate that the analysis of the dependency graph is possible with a reasonable cost in any CDCL.

References

  1. 1.
    Ansótegui, C., Bonnet, M.L., Levy, J., Many, F.: Measuring the hardness of sat instances. In: Proceedings of AAAI, pp. 222–228 (2008)Google Scholar
  2. 2.
    Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: IJCAI (2009)Google Scholar
  3. 3.
    Darwiche, A., Pipatsrisawat, K.: Complete Algorithms, Chap. 3, pp. 99–130. IOS Press (2009)Google Scholar
  4. 4.
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. JACM 5, 394–397 (1962)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005).  https://doi.org/10.1007/11499107_5CrossRefzbMATHGoogle Scholar
  6. 6.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24605-3_37CrossRefGoogle Scholar
  7. 7.
    Huang, J.: The effect of restarts on the efficiency of clause learning. In: IJCAI 2007, pp. 2318–2323 (2007)Google Scholar
  8. 8.
    Järvisalo, M., Matsliah, A., Nordström, J., Živný, S.: Relating proof complexity measures and practical hardness of SAT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 316–331. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33558-7_25CrossRefGoogle Scholar
  9. 9.
    Katsirelos, G., Sabharwal, A., Samulowitz, H., Simon, L.: Resolution and parallelizability: barriers to the efficient parallelization of sat solvers. In: Proceedings of AAAI (2013)Google Scholar
  10. 10.
    Li, C.M., Anbulagan, A.: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of IJCAI, pp. 366–371 (1997)Google Scholar
  11. 11.
    Li, C.M., Gérard, S.: On the limit of branching rules for hard random unsatisfiable 3-sat. In: Proceedings of ECAI, pp. 98–102 (2000)Google Scholar
  12. 12.
    Luo, M., Li, C.M., Xiao, F., Manya, F., Lu, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17), pp. 703–711 (2017)Google Scholar
  13. 13.
    Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530–535 (2001)Google Scholar
  15. 15.
    Piette, C., Hamadi, Y., Sas, L.: Vivifying propositional clausal formulae. In: ECAI, pp. 525–529 (2008)Google Scholar
  16. 16.
    Seidman, S.B.: Network structure and minimum degree. Soc. Netw. 5(3), 269–287 (1983)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Shin, K., Eliassi-Rad, T., Faloutso, C.: Graph mining using k-core analysis - patterns, anomalies and algorithms. In: IEEE 16th International Conference on Data Mining ICMD, pp. 469–478 (2016)Google Scholar
  18. 18.
    Simon, L.: Post mortem analysis of sat solver proofs. In: Berre, D.L. (ed.) POS-14. Fifth Pragmatics of SAT Workshop. EPiC Series in Computing, vol. 27, pp. 26–40. EasyChair (2014).  https://doi.org/10.29007/gpp8, https://easychair.org/publications/paper/N3GD
  19. 19.
    Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09284-3_31CrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.LabriUniversity of BordeauxTalence CedexFrance

Personalised recommendations