Document Open Access Logo

Enumerating All Boolean Matches

Authors Alexander Nadel , Yogev Shalmon

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.22.pdf
  • Filesize: 0.92 MB
  • 21 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.22.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Solvers
Keywords
  • Boolean Matching
  • All-Boolean-Matching
  • Enumeration
  • SAT
  • Generalization

Metrics

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

Abstract

Boolean matching, a fundamental problem in circuit design, determines whether two Boolean circuits are equivalent under input/output permutations and negations. While most works focus on finding a single match or proving its absence, the problem of enumerating all matches remains largely unexplored, with BooM being a notable exception. Motivated by timing challenges in Intel’s library mapping flow, we introduce EBat - an open-source tool for enumerating all matches between single-output circuits. Built from scratch, EBat reuses BooM’s SAT encoding and introduces novel high-level algorithms and performance-critical subroutines to efficiently identify and block multiple mismatches and matches simultaneously. Experiments demonstrate that EBat substantially outperforms BooM’s baseline algorithm, solving 3 to 4 times more benchmarks within a given time limit. EBat has been productized as part of Intel’s library mapping flow, effectively addressing the timing challenges.

Cite As Get BibTex

Alexander Nadel and Yogev Shalmon. Enumerating All Boolean Matches. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.22

Author Details

Alexander Nadel
  • Intel Corporation, Haifa, Israel
  • Faculty of Data and Decision Sciences, Technion, Haifa, Israel
Yogev Shalmon
  • Intel Corporation, Haifa, Israel
  • Faculty of Data and Decision Sciences, Technion, Haifa, Israel

Acknowledgements

We are grateful to Oded Asulin, Yossi Levani, Aviad Munitz, Pavel Nisanov and Hagay Segal for helpful discussions, which played an important role in shaping our research. We also thank Roland Jiang for providing us with the original code for BooM. Additionally, we would like to thank the anonymous reviewers for their valuable comments and insightful suggestions.

Supplementary Materials

References

  1. Afshin Abdollahi. Signature based boolean matching in the presence of don't cares. In Limor Fix, editor, Proceedings of the 45th Design Automation Conference, DAC 2008, Anaheim, CA, USA, June 8-13, 2008, pages 642-647. ACM, 2008. URL: https://doi.org/10.1145/1391469.1391635.
  2. Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, and Alexander Nadel. Sat-based semiformal verification of hardware. 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 25-32. IEEE, 2010. URL: https://ieeexplore.ieee.org/document/5770929/.
  3. Manindra Agrawal and Thomas Thierauf. The boolean isomorphism problem. In 37th Annual Symposium on Foundations of Computer Science, FOCS '96, Burlington, Vermont, USA, 14-16 October, 1996, pages 422-430. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/SFCS.1996.548501.
  4. 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
  5. Daniil Averkov, Tatiana Belova, Gregory Emdin, Mikhail Goncharov, Viktoriia Krivogornitsyna, Alexander S. Kulikov, Fedor Kurmazov, Daniil Levtsov, Georgie Levtsov, Vsevolod Vaskin, and Aleksey Vorobiev. Cirbo: A new tool for boolean circuit analysis and synthesis. Proceedings of the AAAI Conference on Artificial Intelligence, 39(11):11105-11112, April 2025. URL: https://doi.org/10.1609/aaai.v39i11.33207.
  6. Luca Benini and Giovanni De Micheli. A survey of boolean matching techniques for library binding. ACM Transactions on Design Automation of Electronic Systems, 2(3), 1997. URL: https://doi.org/10.1145/264995.264996.
  7. Armin Biere, Daniel Le Berre, Emmanuel Lonca, and Norbert Manthey. Detecting cardinality constraints in CNF. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 285-301. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_22.
  8. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  9. 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
  10. Bernd Borchert, Desh Ranjan, and Frank Stephan. On the computational complexity of some classical equivalence relations on boolean functions. Theory Comput. Syst., 31(6):679-693, 1998. URL: https://doi.org/10.1007/S002240000109.
  11. Daniel Brand. Verification of large synthesized designs. In Michael R. Lightner and Jochen A. G. Jess, editors, Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993, Santa Clara, California, USA, November 7-11, 1993, pages 534-537. IEEE Computer Society / ACM, 1993. URL: https://doi.org/10.1109/ICCAD.1993.580110.
  12. Robert K. Brayton and Alan Mishchenko. ABC: an academic industrial-strength verification tool. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 24-40. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_5.
  13. Franc Brglez and Hideo Fujiwara. A neutral netlist of 10 combinational benchmark circuits and a target translator. In Fortran. ISCAS’85, 1985. Google Scholar
  14. 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.
  15. Chung-Han Chou, Chih-Jen Jacky Hsu, Chi-An Rocky Wu, Kuan-Hua Tu, and Kei-Yong Khoo. Invited paper: 2023 iccad cad contest problem a: Multi-bit large-scale boolean matching. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 1-4, 2023. URL: https://doi.org/10.1109/ICCAD57390.2023.10323797.
  16. Jason Cong and Yean-Yow Hwang. Boolean matching for lut-based logic blocks with applications toarchitecture evaluation and technology mapping. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 20(9):1077-1090, 2001. URL: https://doi.org/10.1109/43.945303.
  17. F. Corno, M.S. Reorda, and G. Squillero. Rt-level itc'99 benchmarks and first atpg results. IEEE Design & Test of Computers, 17(3):44-53, 2000. URL: https://doi.org/10.1109/54.867894.
  18. Nachum Dershowitz, Ziyad Hanna, and Alexander Nadel. A scalable algorithm for minimal unsatisfiable core extraction. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 36-41. Springer, 2006. URL: https://doi.org/10.1007/11814948_5.
  19. 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. URL: http://dl.acm.org/citation.cfm?id=2157675.
  20. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing, 6th International Conference, SAT, Proceedings, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  21. Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing generalization boosts enumeration. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 13:1-13:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.SAT.2024.13.
  22. Shao-Lun Huang, Wei-Hsun Lin, Po-Kai Huang, and Chung-Yang Huang. Match and replace: A functional ECO engine for multierror circuit rectification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 32(3):467-478, 2013. URL: https://doi.org/10.1109/TCAD.2012.2226456.
  23. Zheng Huang, Lingli Wang, Yakov Nasikovskiy, and Alan Mishchenko. Fast boolean matching based on NPN classification. In 2013 International Conference on Field-Programmable Technology, FPT 2013, Kyoto, Japan, December 9-11, 2013, pages 310-313. IEEE, 2013. URL: https://doi.org/10.1109/FPT.2013.6718374.
  24. 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. URL: https://doi.org/10.1147/SJ.83.0178.
  25. Chih Fan Lai, Jie Hong R. Jiang, and Kuo Hua Wang. Boolean matching of function vectors with strengthened learning. In IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD, 2010. URL: https://doi.org/10.1109/ICCAD.2010.5654215.
  26. Chih Fan Lai, Jie Hong R. Jiang, and Kuo Hua Wang. BooM: A decision procedure for Boolean matching with abstraction and dynamic learning. In Proceedings - Design Automation Conference, 2010. URL: https://doi.org/10.1145/1837274.1837398.
  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. Alan Mishchenko, Supratik Chatterjee, Robert Brayton, Xiangjian Wang, and Tony Kam. Technology mapping with boolean matching, supergates and choices. Technical report, EECS Department, University of California, Berkeley, March 2005. Google Scholar
  29. Janett Mohnke, Paul Molitor, and Sharad Malik. Application of bdds in boolean matching techniques for formal logic combinational verification. Int. J. Softw. Tools Technol. Transf., 3(2):207-216, 2001. URL: https://doi.org/10.1007/S100090100039.
  30. 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. URL: https://doi.org/10.23919/FMCAD.2019.8894273.
  31. Alexander Nadel. Polarity and variable selection heuristics for sat-based anytime maxsat. J. Satisf. Boolean Model. Comput., 12(1):17-22, 2020. URL: https://doi.org/10.3233/SAT-200126.
  32. 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.
  33. Alexander Nadel and Vadim Ryvchin. Efficient SAT solving under assumptions. In Theory and Applications of Satisfiability Testing - SAT, Proceedings, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_19.
  34. Emil L. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 43, 1921. Google Scholar
  35. 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.
  36. Franz-Xaver Reichl, Friedrich Slivovsky, and Stefan Szeider. eslim: Circuit minimization with SAT based local improvement. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 23:1-23:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.SAT.2024.23.
  37. 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.
  38. Roberto Sebastiani. Are you satisfied by this partial assignment? CoRR, abs/2003.04225, 2020. URL: https://arxiv.org/abs/2003.04225.
  39. 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.
  40. Pawel Swierczynski, Marc Fyrbiak, Christof Paar, Christophe Huriaux, and Russell Tessier. Protecting against cryptographic trojans in fpgas. In 23rd IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, FCCM 2015, Vancouver, BC, Canada, May 2-6, 2015, pages 151-154. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FCCM.2015.55.
  41. 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
  42. Kuo-Hua Wang, Chung-Ming Chan, and Jung-Chang Liu. Simulation and sat-based boolean matching for large boolean networks. In Proceedings of the 46th Design Automation Conference, DAC 2009, San Francisco, CA, USA, July 26-31, 2009, pages 396-401. ACM, 2009. URL: https://doi.org/10.1145/1629911.1630016.
  43. Chaofan Yu, Lingli Wang, Chun Zhang, Yu Hu, and Lei He. Fast filter-based boolean matchers. IEEE Embed. Syst. Lett., 5(4):65-68, 2013. URL: https://doi.org/10.1109/LES.2013.2280582.
  44. Juling Zhang, Guowu Yang, William N. N. Hung, and Jinzhao Wu. A canonical-based NPN boolean matching algorithm utilizing boolean difference and cofactor signature. IEEE Access, 5:27777-27785, 2017. URL: https://doi.org/10.1109/ACCESS.2017.2778338.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact