Document Open Access Logo

Entailing Generalization Boosts Enumeration

Authors Dror Fried , Alexander Nadel , Roberto Sebastiani , Yogev Shalmon

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.13.pdf
  • Filesize: 0.88 MB
  • 14 pages

Document Identifiers

Author Details

Dror Fried
  • Department of Mathematics and Computer Science, The Open University of Israel, Ra’anana, Israel
Alexander Nadel
  • Intel Corporation, Israel and Faculty of Data and Decision Sciences, Technion, Haifa, Israel
Roberto Sebastiani
  • DISI, University of Trento, Italy
Yogev Shalmon
  • Intel Corporation, Israel and The Open University of Israel, Ra’anana, Israel

Funding

We acknowledge the support of the MUR PNRR project FAIR - Future AI Research (PE00000013), under the NRRP MUR program funded by the NextGenerationEU. The work was partially supported by the project "AI@TN" funded by the Autonomous Province of Trento. Also funded in part by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Health and Digital Executive Agency (HaDEA). Neither the European Union nor the granting authority can be held responsible for them. Grant Agreement no. 101120763 - TANGO.
  • Shalmon, Yogev: This research was supported by The Open University of Israel’s Research Fund.

Acknowledgements

We are grateful to Ben Emanuel for helpful discussions which played an important role in shaping our research. Also, we thank the anonymous reviewers for their comments and useful suggestions.

Cite AsGet BibTex

Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.13

Abstract

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Solvers
Keywords
  • Generalization
  • Minimization
  • Prime Implicant
  • AllSAT
  • SAT
  • Circuits

Metrics

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

Supplementary Materials

References

  1. Luca Amarú, Pierre-Emmanuel Gaillardon, and Giovanni De Micheli. The EPFL combinational benchmark suite. In Proceedings of the 24th International Workshop on Logic & Synthesis (IWLS), 2015. Google Scholar
  2. Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023. Google Scholar
  3. Jeremias Berg, Matti Järvisalo, Ruben Martins, and Andreas Niskanen, editors. MaxSAT Evaluation 2023: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023. Google Scholar
  4. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, volume B-2020-1 of Department of Computer Science Report Series B, pages 51-53. University of Helsinki, 2020. Google Scholar
  5. Armin Biere, Keijo Heljanko, and Siert Wieringa. AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2011. Google Scholar
  6. Aaron R. Bradley. Sat-based model checking without unrolling. In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 70-87. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-18275-4_7.
  7. T. Castell. Computation of prime implicates and prime implicants by a variant of the davis and putnam procedure. In Proceedings Eighth IEEE International Conference on Tools with Artificial Intelligence, pages 428-429, 1996. URL: https://doi.org/10.1109/TAI.1996.560739.
  8. Hana Chockler, Alexander Ivrii, Arie Matsliah, Shiri Moran, and Ziv Nevo. Incremental formal verification of hardware. In Per Bjesse and Anna Slobodová, editors, International Conference on Formal Methods in Computer-Aided Design, FMCAD '11, Austin, TX, USA, October 30 - November 02, 2011, pages 135-143. FMCAD Inc., 2011. URL: http://dl.acm.org/citation.cfm?id=2157676.
  9. Alejandro Czutro, Ilia Polian, Piet Engelke, Sudhakar M. Reddy, and Bernd Becker. Dynamic compaction in sat-based ATPG. In Proceedings of the Eighteentgh Asian Test Symposium, ATS 2009, 23-26 November 2009, Taichung, Taiwan, pages 187-190. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/ATS.2009.31.
  10. David Déharbe, Pascal Fontaine, Daniel Le Berre, and Bertrand Mazure. Computing prime implicants. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 46-52. IEEE, 2013. URL: https://ieeexplore.ieee.org/document/6679390/.
  11. Imen Ouled Dlala, Saïd Jabbour, Lakhdar Saïs, and Boutheina Ben Yaghlane. A comparative study of SAT-based itemsets mining. In Research and Development in Intelligent Systems XXXIII - Incorporating Applications and Innovations in Intelligent Systems XXIV. Proceedings of AI-2016., pages 37-52, 2016. Google Scholar
  12. Niklas Eén, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125-134, 2011. Google Scholar
  13. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT, Proceedings, 2003. Google Scholar
  14. Dror Fried, Alexander Nadel, and Yogev Shalmon. AllSAT for combinational circuits. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 9:1-9:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.9.
  15. Alexandra Goultiaeva and Fahiem Bacchus. Exploiting QBF duality on a circuit representation. In Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, 2010. URL: https://doi.org/10.1609/AAAI.V24I1.7548.
  16. James S. Jephson, Robert P. McQuarrie, and Robert E. Vogelsberg. A three-value computer design verification system. IBM Systems Journal, 8(3):178-188, 1969. Google Scholar
  17. HoonSang Jin, HyoJung Han, and Fabio Somenzi. Efficient conflict analysis for finding all satisfying assignments of a boolean circuit. In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 287-300. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31980-1_19.
  18. HoonSang Jin and Fabio Somenzi. Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In Proceedings of the 42nd Design Automation Conference, DAC, 2005. Google Scholar
  19. Alex Kean and George K. Tsiknis. An incremental method for generating prime implicants/impicates. J. Symb. Comput., 9(2):185-206, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80029-6.
  20. Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, and Daniel Jackson. A case for efficient solution enumeration. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT, 2003. Google Scholar
  21. Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, and Moshe Y. Vardi. Safety model checking with complementary approximations. In Sri Parameswaran, editor, 2017 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2017, Irvine, CA, USA, November 13-16, 2017, pages 95-100. IEEE, 2017. URL: https://doi.org/10.1109/ICCAD.2017.8203765.
  22. Nuno P Lopes, Nikolaj Bjørner, Patrice Godefroid, and George Varghese. Network verification in the light of program verification. MSR, Rep, 2013. Google Scholar
  23. Weilin Luo, Hai Wan, Hongzhen Zhong, Ou Wei, Biqing Fang, and Xiaotong Song. An efficient two-phase method for prime compilation of non-clausal boolean formulae. In IEEE/ACM International Conference On Computer Aided Design, ICCAD 2021, pages 1-9. IEEE, 2021. URL: https://doi.org/10.1109/ICCAD51958.2021.9643520.
  24. Inês Lynce and João Marques-Silva. On computing minimum unsatisfiable cores. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/110.pdf.
  25. Norbert Manthey. The mergesat solver. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 387-398. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_27.
  26. Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani. On CNF conversion for disjoint SAT enumeration. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 15:1-15:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.15.
  27. E. J. McCluskey. Minimization of boolean functions. The Bell System Technical Journal, 35(6):1417-1444, 1956. URL: https://doi.org/10.1002/j.1538-7305.1956.tb03835.x.
  28. Kenneth L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Computer Aided Verification, 14th International Conference, CAV, Proceedings, 2002. Google Scholar
  29. Sibylle Möhle and Armin Biere. Dualizing projected model counting. In IEEE 30th International Conference on Tools with Artificial Intelligence, ICTAI, pages 702-709, 2018. URL: https://doi.org/10.1109/ICTAI.2018.00111.
  30. Sibylle Möhle, Roberto Sebastiani, and Armin Biere. Four flavors of entailment. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 62-71. Springer, July 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_5.
  31. Sibylle Möhle, Roberto Sebastiani, and Armin Biere. On enumerating short projected models. CoRR, abs/2110.12924, October 2021. URL: https://arxiv.org/abs/2110.12924.
  32. Alexander Nadel. Boosting minimal unsatisfiable core extraction. In Roderick Bloem and Natasha Sharygina, editors, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 221-229. IEEE, 2010. URL: https://ieeexplore.ieee.org/document/5770953/.
  33. Alexander Nadel. Anytime weighted MaxSAT with improved polarity selection and bit-vector optimization. In Formal Methods in Computer Aided Design, FMCAD, Proceedings, pages 193-202, 2019. Google Scholar
  34. Alexander Nadel. Polarity and variable selection heuristics for SAT-based anytime MaxSAT. Journal on Satisfiability, Boolean Modeling and Computation, 2020. Google Scholar
  35. Alexander Nadel. Introducing intel(r) SAT solver. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 8:1-8:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.8.
  36. Alexander Nadel and Vadim Ryvchin. Efficient SAT solving under assumptions. In Theory and Applications of Satisfiability Testing - SAT, Proceedings, 2012. Google Scholar
  37. Emil L. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 43, 1921. Google Scholar
  38. Alessandro Previti, Alexey Ignatiev, António Morgado, and João Marques-Silva. Prime compilation of non-clausal formulae. In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 1980-1988. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/281.
  39. W. V. Quine. The problem of simplifying truth functions. The American Mathematical Monthly, 59(8):521-531, 1952. URL: https://doi.org/10.1080/00029890.1952.11988183.
  40. Kavita Ravi and Fabio Somenzi. Minimal assignments for bounded model checking. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2988 of Lecture Notes in Computer Science, pages 31-45. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_3.
  41. J. Paul Roth, Willard G. Bouricius, and Peter R. Schneider. Programmed algorithms to compute tests to detect and distinguish between failures in logic circuits. IEEE Trans. Electron. Comput., 16(5):567-580, 1967. URL: https://doi.org/10.1109/PGEC.1967.264743.
  42. Roberto Sebastiani. Are you satisfied by this partial assignment? CoRR, abs/2003.04225, February 2020. URL: https://arxiv.org/abs/2003.04225.
  43. Tobias Seufert, Felix Winterer, Christoph Scholl, Karsten Scheibler, Tobias Paxian, and Bernd Becker. Everything you always wanted to know about generalization of proof obligations in PDR. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 42(4):1351-1364, 2023. URL: https://doi.org/10.1109/TCAD.2022.3198260.
  44. James R. Slagle, Chin-Liang Chang, and Richard C. T. Lee. A new algorithm for generating prime implicants. IEEE Trans. Computers, 19(4):304-310, 1970. URL: https://doi.org/10.1109/T-C.1970.222917.
  45. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  46. Robert B. Hitchcock Sr. Timing verification and the timing analysis program. In Proceedings of the 19th Design Automation Conference, DAC, 1982. Google Scholar
  47. P. Tafertshofer and A. Ganz. Sat based atpg using fast justification and propagation in the implication graph. In 1999 IEEE/ACM International Conference on Computer-Aided Design. Digest of Technical Papers (Cat. No.99CH37051), pages 139-146, 1999. URL: https://doi.org/10.1109/ICCAD.1999.810638.
  48. Abraham Temesgen Tibebu and Görschwin Fey. Augmenting all solution SAT solving for circuits with structural information. In 21st IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, DDECS 2018, Budapest, Hungary, April 25-27, 2018, pages 117-122. IEEE, 2018. URL: https://doi.org/10.1109/DDECS.2018.00028.
  49. Takahisa Toda and Takehide Soh. Implementing efficient all solutions SAT solvers. Journal of Experimental Algorithmics (JEA), 2016. Google Scholar
  50. Grigori S Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967-1970, pages 466-483, 1983. Google Scholar
  51. Yakir Vizel and Arie Gurfinkel. Interpolating property directed reachability. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 260-276. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_17.
  52. Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, and Sharad Malik. All-SAT using minimal blocking clauses. Proceedings of the IEEE International Conference on VLSI Design, pages 86-91, 2014. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact