Document Open Access Logo

Explaining SAT Solving Using Causal Reasoning

Authors Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, Kuldeep S. Meel



PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.28.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Jiong Yang
  • National University of Singapore, Singapore
Arijit Shaw
  • Chennai Mathematical Institute, India
  • IAI, TCG-CREST, Kolkata, India
Teodora Baluta
  • National University of Singapore, Singapore
Mate Soos
  • National University of Singapore, Singapore
Kuldeep S. Meel
  • National University of Singapore, Singapore

Acknowledgements

We are thankful to Tim van Bremen for providing detailed feedback on the early drafts of the paper and grateful to the anonymous reviewers for their constructive comments to improve this paper. We extend sincere gratitude to Jakob Nordström and other participants of the program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theory of Computing for insightful discussions. Part of the work was done during Arijit Shaw’s internship at the National University of Singapore. The computational work for this article was performed on resources of the National Supercomputing Centre, Singapore, https://www.nscc.sg.

Cite AsGet BibTex

Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 28:1-28:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.28

Abstract

The past three decades have witnessed notable success in designing efficient SAT solvers, with modern solvers capable of solving industrial benchmarks containing millions of variables in just a few seconds. The success of modern SAT solvers owes to the widely-used CDCL algorithm, which lacks comprehensive theoretical investigation. Furthermore, it has been observed that CDCL solvers still struggle to deal with specific classes of benchmarks comprising only hundreds of variables, which contrasts with their widespread use in real-world applications. Consequently, there is an urgent need to uncover the inner workings of these seemingly weak yet powerful black boxes. In this paper, we present a first step towards this goal by introducing an approach called {CausalSAT}, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. {CausalSAT} initially generates observational data from the execution of SAT solvers and learns a structured graph representing the causal relationships between the components of a SAT solver. Subsequently, given a query such as whether a clause with low literals blocks distance (LBD) has a higher clause utility, {CausalSAT} calculates the causal effect of LBD on clause utility and provides an answer to the question. We use {CausalSAT} to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings, such as the query above or the notion that clauses with high LBD experience a rapid drop in utility over time. Moreover, {CausalSAT} can address previously unexplored questions, like which branching heuristic leads to greater clause utility in order to study the relationship between branching and clause management. Experimental evaluations using practical benchmarks demonstrate that {CausalSAT} effectively fits the data, verifies four "rules of thumb", and provides answers to three questions closely related to implementing modern solvers.

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Computing methodologies → Artificial intelligence
Keywords
  • Satisfiability
  • Causality
  • SAT solver
  • Clause management

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Kartik Ahuja, Yixin Wang, Divyat Mahajan, and Yoshua Bengio. Interventional causal representation learning. In Proc. of NeurIPS Workshop on Causality for Real-world Impact, 2022. Google Scholar
  2. Martin Arjovsky, Léon Bottou, Ishaan Gulrajani, and David Lopez-Paz. Invariant risk minimization. arXiv preprint, 2019. URL: https://arxiv.org/abs/1907.02893.
  3. Gilles Audemard and Laurent Simon. Glucose: a solver that predicts learnt clauses quality. SAT Competition, 2009. Google Scholar
  4. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Proc. of IJCAI, 2009. Google Scholar
  5. Gilles Audemard and Laurent Simon. On the glucose SAT solver. International Journal on Artificial Intelligence Tools, 2018. Google Scholar
  6. Armin Biere. Lingeling, Plingeling and Treengeling entering the SAT competition 2013. Proc. of SAT competition, 2013. Google Scholar
  7. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In Proc. of TACAS, 1999. Google Scholar
  8. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Proc. of SAT Competition - Solver and Benchmark Descriptions, 2020. Google Scholar
  9. Armin Biere and Andreas Fröhlich. Evaluating CDCL variable scoring schemes. In Proc. of DAC, 2015. Google Scholar
  10. Johann Brehmer, Pim De Haan, Phillip Lippe, and Taco Cohen. Weakly supervised causal representation learning. In Proc. of UAI Workshop on Causal Representation Learning, 2022. Google Scholar
  11. Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Proc. of TACAS, 2004. Google Scholar
  12. Diego Colombo and Marloes H. Maathuis. Order-Independent Constraint-Based Causal Structure Learning. Journal of Machine Learning Research, 2014. Google Scholar
  13. Stephen A Cook. The complexity of theorem-proving procedures. In Proc. of STOC, 1971. Google Scholar
  14. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 1962. Google Scholar
  15. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Proc. of SAT, 2003. Google Scholar
  16. Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, and Laurent Simon. Seeking practical cdcl insights from theoretical sat benchmarks. In IJCAI, pages 1300-1308, 2018. Google Scholar
  17. Laurent Simon Gilles Audemard. Glucose 1.0, 2009. sources/glucose/core/Solver.C:Lines 631-635. URL: https://www.labri.fr/perso/lsimon/downloads/softwares/glucose_1.0.zip.
  18. Carla P Gomes, Bart Selman, Henry Kautz, et al. Boosting combinatorial search through randomization. Proc. of AAAI/IAAI, 1998. Google Scholar
  19. Jinbo Huang et al. The Effect of Restarts on the Efficiency of Clause Learning. In Proc. of IJCAI, 2007. Google Scholar
  20. Yimin Huang and Marco Valtorta. Pearl’s calculus of intervention is complete. In Proc. of UAI, 2006. Google Scholar
  21. Matti Järvisalo, Daniel Le Berre, Olivier Roussel, and Laurent Simon. The international SAT solver competitions. AI Magazine, 2012. Google Scholar
  22. Henry A Kautz, Bart Selman, et al. Planning as Satisfiability. In Proc. of ECAI, 1992. Google Scholar
  23. Janne I Kokkala and Jakob Nordström. Using resolution proofs to analyse CDCL solvers. In Proc. of CP, 2020. Google Scholar
  24. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Proc. of SAT, 2016. Google Scholar
  25. Jia Hui Liang, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, and Vijay Ganesh. Machine learning-based restart policy for CDCL SAT solvers. In Proc. of SAT, 2018. Google Scholar
  26. Jia Hui Liang, Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh. An empirical study of branching heuristics through the lens of global learning rate. In Proc. of SAT, 2017. Google Scholar
  27. Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of Las Vegas algorithms. Information Processing Letters, 1993. Google Scholar
  28. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manya, and Zhipeng Lü. An effective learnt clause minimization approach for CDCL SAT solvers. In Proc. of IJCAI, 2017. Google Scholar
  29. Inês Lynce and Joao Marques-Silva. SAT in bioinformatics: Making the case with haplotype inference. In Proc. of SAT, 2006. Google Scholar
  30. João P Marques-Silva and Karem A Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 1999. Google Scholar
  31. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proc. of DAC, 2001. Google Scholar
  32. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In Proc. of SAT, 2018. Google Scholar
  33. Chanseok Oh. Between SAT and UNSAT: the fundamental difference in CDCL SAT. In Proc. of SAT, 2015. Google Scholar
  34. Chanseok Oh. Improving SAT solvers by exploiting empirical characteristics of CDCL. PhD thesis, New York University, 2016. Google Scholar
  35. Judea Pearl. Causal inference in statistics: An overview. Statistics Surveys, 2009. Google Scholar
  36. Judea Pearl. Causality. Cambridge University Press, 2009. Google Scholar
  37. Jonas Peters, Peter Bühlmann, and Nicolai Meinshausen. Causal inference by using invariant prediction: identification and confidence intervals. Journal of the Royal Statistical Society. Series B (Statistical Methodology), pages 947-1012, 2016. Google Scholar
  38. Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In Proc. of SAT, 2007. Google Scholar
  39. Bernhard Schölkopf, Francesco Locatello, Stefan Bauer, Nan Rosemary Ke, Nal Kalchbrenner, Anirudh Goyal, and Yoshua Bengio. Toward causal representation learning. Proc. of IEEE, 109(5):612-634, 2021. Google Scholar
  40. Gideon Schwarz. Estimating the dimension of a model. The Annals of Statistics, 1978. Google Scholar
  41. Marco Scutari. Learning Bayesian Networks with the bnlearn R Package. Journal of Statistical Software, 2010. Google Scholar
  42. Marco Scutari and Radhakrishnan Nagarajan. Identifying significant edges in graphical models of molecular networks. Artificial Intelligence in Medicine, 2013. Google Scholar
  43. Amit Sharma, Emre Kiciman, et al. DoWhy: A Python package for causal inference, 2019. URL: https://github.com/microsoft/dowhy.
  44. Qiang Shen and Rónán Daly. Methods to accelerate the learning of bayesian network structures. In Proc. of UK Workshop on Computational Intelligence, 2007. Google Scholar
  45. JP Marques Silva and Karem A Sakallah. Conflict analysis in search algorithms for satisfiability. In Proc. of ICTAI, 1996. Google Scholar
  46. Laurent Simon. Post mortem analysis of sat solver proofs. In POS@ SAT, pages 26-40, 2014. Google Scholar
  47. Mate Soos, Jo Devriendt, Stephan Gocht, Arijit Shaw, and Kuldeep S Meel. Cryptominisat with CCAnr at the SAT competition 2020. SAT COMPETITION, 2020. Google Scholar
  48. Mate Soos, Raghav Kulkarni, and Kuldeep S Meel. CrystalBall: Gazing in the Black Box of SAT Solving. In Proc. of SAT, 2019. Google Scholar
  49. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Proc. of SAT, 2009. Google Scholar
  50. Toby Walsh. Search in a small world. In Proc. of IJCAI, pages 1172-1177, 1999. Google Scholar
  51. Ruoyu Wang, Mingyang Yi, Zhitang Chen, and Shengyu Zhu. Out-of-distribution generalization with causal invariant transformations. In Proc. of CVPR, pages 375-385, 2022. Google Scholar
  52. Nathan Wetzler, Marijn JH Heule, and Warren A Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Proc. of SAT, 2014. Google Scholar
  53. Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. SATzilla: portfolio-based algorithm selection for SAT. Journal of artificial intelligence research, 2008. Google Scholar
  54. Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining sat solving using causal reasoning. arXiv, 2023. URL: https://arxiv.org/abs/2306.06294.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail