Document Open Access Logo

AllSAT for Combinational Circuits

Authors Dror Fried, Alexander Nadel , Yogev Shalmon

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.9.pdf
  • Filesize: 0.83 MB
  • 18 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, Haifa, Israel
  • Faculty of Data and Decision Sciences, Technion, Haifa, Israel
Yogev Shalmon
  • Intel Corporation, Haifa, Israel
  • The Open University of Israel, Ra’anana, Israel

Funding

  • Shalmon, Yogev: This research was partially supported by The Open University of Israel's Research Fund (grant no. 41662).

Acknowledgements

We are grateful to Supratik Chakraborty, Alexander Ivrii, Kuldeep Meel, Roberto Sebastiani, Mate Soos and Moshe Vardi 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, and Yogev Shalmon. AllSAT for Combinational Circuits. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.9

Abstract

Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Solvers
Keywords
  • 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. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiabiliy. In Handbook of Satisfiability - Second Edition, pages 929-991. IOS Press, 2021. Google Scholar
  3. 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
  4. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. Google Scholar
  5. Randal E. Bryant, Derek L. Beatty, Karl S. Brace, Kyeongsoon Cho, and Thomas J. Sheffler. COSMOS: A compiled simulator for MOS circuits. In Proceedings of the 24th ACM/IEEE Design Automation Conference, pages 9-16, 1987. Google Scholar
  6. Randall E Bryant. Race detection in mos circuits by ternary simulation, 1983. Google Scholar
  7. 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
  8. 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
  9. 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
  10. Anders Franzén. Efficient Solving of the Satisfiability Modulo Bit-Vectors Problem and Some Extensions to SMT. PhD thesis, University of Trento, Italy, 2010. Google Scholar
  11. Malay K Ganai, Aarti Gupta, and Pranav Ashar. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In IEEE/ACM International Conference on Computer Aided Design,ICCAD., pages 510-517, 2004. Google Scholar
  12. 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: http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1791.
  13. Alberto Griggio and Marco Roveri. Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 35(6):1026-1039, 2016. URL: https://doi.org/10.1109/TCAD.2015.2481869.
  14. Orna Grumberg, Assaf Schuster, and Avi Yadgar. Memory efficient all-solutions SAT solver and its application for reachability analysis. In Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD, Proceedings, 2004. Google Scholar
  15. Arie Gurfinkel and Alexander Ivrii. Pushing to the top. In Formal Methods in Computer-Aided Design, FMCAD, pages 65-72, 2015. Google Scholar
  16. Zyad Hassan, Aaron R Bradley, and Fabio Somenzi. Better generalization in ic3. In 2013 Formal Methods in Computer-Aided Design, pages 157-164, 2013. Google Scholar
  17. Jinbo Huang and Adnan Darwiche. The language of search. J. Artif. Intell. Res., 29:191-219, 2007. Google Scholar
  18. 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
  19. HoonSang Jin, HyoJung Han, and Fabio Somenzi. Efficient conflict analysis for finding all satisfying assignments of a boolean circuit. In Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS, Proceedings, 2005. URL: https://doi.org/10.1007/978-3-540-31980-1_19.
  20. 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
  21. Daher Kaiss, Marcelo Skaba, Ziyad Hanna, and Zurab Khasidashvili. Industrial strength SAT-based alignability algorithm for hardware equivalence verification. In Formal Methods in Computer Aided Design (FMCAD), pages 20-26, 2007. Google Scholar
  22. 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
  23. Petr Kucera and Petr Savický. Backdoor decomposable monotone circuits and their propagation complete encodings. CoRR, abs/1811.09435, 2018. URL: https://arxiv.org/abs/1811.09435.
  24. Bin Li, Michael S. Hsiao, and Shuo Sheng. A novel SAT all-solutions solver for efficient preimage computation. In 2004 Design, Automation and Test in Europe Conference and Exposition, pages 272-279, 2004. Google Scholar
  25. Jiaxin Liang, Feifei Ma, Junping Zhou, and Minghao Yin. Allsatcc: Boosting AllSAT solving with efficient component analysis. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI, 2022. Google Scholar
  26. Nuno P Lopes, Nikolaj Bjørner, Patrice Godefroid, and George Varghese. Network verification in the light of program verification. MSR, Rep, 2013. Google Scholar
  27. 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.
  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. A. Morgado and J. Marques-Silva. Good learning and implicit model enumeration. Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI, pages 131-136, 2005. Google Scholar
  31. 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
  32. Alexander Nadel. Polarity and variable selection heuristics for SAT-based anytime MaxSAT. Journal on Satisfiability, Boolean Modeling and Computation, 2020. Google Scholar
  33. Alexander Nadel. Introducing intel(r) SAT solver. In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT, 2022. Google Scholar
  34. Alexander Nadel and Vadim Ryvchin. Efficient SAT solving under assumptions. In Theory and Applications of Satisfiability Testing - SAT, Proceedings, 2012. Google Scholar
  35. Emil L. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 43, 1921. Google Scholar
  36. 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.
  37. Sven Reimer, Matthias Sauer, Paolo Marin, and Bernd Becker. QBF with soft variables. Electronic Communications of the EASST, 70, 2014. Google Scholar
  38. Jan-Willem Roorda and Koen Claessen. SAT-based assistance in abstraction refinement for symbolic trajectory evaluation. In Computer Aided Verification, 18th International Conference, CAV, Proceedings, 2006. Google Scholar
  39. Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, and Bernd Becker. Provably optimal test cube generation using quantified boolean formula solving. In 18th Asia and South Pacific Design Automation Conference, ASP-DAC, 2013. Google Scholar
  40. 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. under submission. CoRR, abs/2105.09169, 2021. URL: https://arxiv.org/abs/2105.09169.
  41. James R. Slagle, Chin-Liang Chang, and Richard C. T. Lee. A new algorithm for generating prime implicants. IEEE Trans. Computers, 1970. URL: https://doi.org/10.1109/T-C.1970.222917.
  42. Robert B. Hitchcock Sr. Timing verification and the timing analysis program. In Proceedings of the 19th Design Automation Conference, DAC, 1982. Google Scholar
  43. 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, pages 117-122. IEEE, 2018. URL: https://doi.org/10.1109/DDECS.2018.00028.
  44. Takahisa Toda and Takehide Soh. Implementing efficient all solutions SAT solvers. Journal of Experimental Algorithmics (JEA), 2016. Google Scholar
  45. 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
  46. 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
  47. Yueling Zhang, Geguang Pu, and Jun Sun. Accelerating All-SAT computation with short blocking clauses. In 35th IEEE/ACM International Conference on Automated Software Engineering, ASE, 2020. 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