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.
This work was supported by the French Project SATAS ANR-15-CE40-0017.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For the reviewing process, figures are in colors. We plan to make two versions of the paper if accepted, with a black and white version of the figures for the proceedings.
References
Ansótegui, C., Bonnet, M.L., Levy, J., Many, F.: Measuring the hardness of sat instances. In: Proceedings of AAAI, pp. 222–228 (2008)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solvers. In: IJCAI (2009)
Darwiche, A., Pipatsrisawat, K.: Complete Algorithms, Chap. 3, pp. 99–130. IOS Press (2009)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. JACM 5, 394–397 (1962)
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_5
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_37
Huang, J.: The effect of restarts on the efficiency of clause learning. In: IJCAI 2007, pp. 2318–2323 (2007)
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_25
Katsirelos, G., Sabharwal, A., Samulowitz, H., Simon, L.: Resolution and parallelizability: barriers to the efficient parallelization of sat solvers. In: Proceedings of AAAI (2013)
Li, C.M., Anbulagan, A.: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of IJCAI, pp. 366–371 (1997)
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)
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)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of DAC, pp. 530–535 (2001)
Piette, C., Hamadi, Y., Sas, L.: Vivifying propositional clausal formulae. In: ECAI, pp. 525–529 (2008)
Seidman, S.B.: Network structure and minimum degree. Soc. Netw. 5(3), 269–287 (1983)
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)
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
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_31
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Fossé, R., Simon, L. (2018). On the Non-degeneracy of Unsatisfiability Proof Graphs Produced by SAT Solvers. 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_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-98334-9_9
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)