Document Open Access Logo

Clausal Congruence Closure

Authors Armin Biere , Katalin Fazekas , Mathias Fleury , Nils Froleyks

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.6.pdf
  • Filesize: 1.24 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Satisfiability Solving
  • Congruence Closure
  • Structural Hashing
  • SAT Sweeping
  • Conjunctive Normal Form
  • Combinational Equivalence Checking
  • Hardware Equivalence Checking

Metrics

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

Abstract

Many practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance.

Cite As Get BibTex

Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.6

Author Details

Armin Biere
  • University Freiburg, Germany
Katalin Fazekas
  • TU Wien, Austria
Mathias Fleury
  • University Freiburg, Germany
Nils Froleyks
  • Johannes Kepler University, Linz, Austria

Funding

This work was supported by the state of Baden-Württemberg through bwHPC, the German Research Foundation (DFG) through grant INST 35/1597-1 FUGG, the Austrian Science Fund (FWF) under project No. T-1306, and by a gift from Intel Corporation.

Acknowledgements

Finally, we want to thank the anonymous reviewers for valuable comments and useful suggestions, which definitely helped us to improve the paper considerably, particularly in the exposition of the experimental part.

Supplementary Materials

References

  1. Luca G. Amarù, Felipe S. Marranghello, Eleonora Testa, Christopher Casares, Vinicius N. Possani, Jiong Luo, Patrick Vuillod, Alan Mishchenko, and Giovanni De Micheli. Sat-sweeping enhanced for logic synthesis. In 57th ACM/IEEE Design Automation Conference, DAC 2020, San Francisco, CA, USA, July 20-24, 2020, pages 1-6. IEEE, 2020. URL: https://doi.org/10.1109/DAC18072.2020.9218691.
  2. Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett., 8(3):121-123, 1979. URL: https://doi.org/10.1016/0020-0190(79)90002-4.
  3. Fahiem Bacchus. Enhancing Davis Putnam with extended binary clause reasoning. In Rina Dechter, Michael J. Kearns, and Richard S. Sutton, editors, Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, pages 613-619. AAAI Press / The MIT Press, 2002. Google Scholar
  4. Fahiem Bacchus and Jonathan Winter. Effective preprocessing with hyper-resolution and equality reduction. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 341-355. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_26.
  5. Tomás Balyo, Andreas Fröhlich, Marijn Heule, and Armin Biere. Everything you always wanted to know about blocked sets (but were afraid to ask). 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 317-332. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_24.
  6. Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Congruence closure with free variables. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II, volume 10206 of Lecture Notes in Computer Science, pages 214-230, 2017. URL: https://doi.org/10.1007/978-3-662-54580-5_13.
  7. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267-1329. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201017.
  8. Armin Biere. The AIGER And-Inverter Graph (AIG) format version 20071012. Technical Report 07/1, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2007. Google Scholar
  9. Armin Biere. Pre,icoSAT@SC'09. In SAT 2009 Competitive Event Booklet, 2009. URL: http://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf.
  10. Armin Biere. Lingeling and friends entering the SAT Challenge 2012. In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proc. of SAT Challenge 2012: Solver and Benchmark Descriptions, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 33-34. Univ.Helsinki, 2012. Google Scholar
  11. Armin Biere. Yet another local search solver and Lingeling and friends entering the SAT Competition 2014. In Adrian Balint, Andon Belov, Marijn Heule, and Matti Järvisalo, editors, Proc. of SAT Competition 2014 - Solver and Benchmark Descriptions, volume B-2014-2 of Department of Computer Science Series of Publications B, pages 39-40. Univ.Helsinki, 2014. Google Scholar
  12. Armin Biere. Collection of combinational arithmetic miters submitted to the SAT Competition 2016. In Tomáš Balyo, Marijn Heule, and Matti Järvisalo, editors, Proc. of SAT Competition 2016 - Solver and Benchmark Descriptions, volume B-2016-1 of Department of Computer Science Series of Publications B, pages 65-66. Univ.Helsinki, 2016. Google Scholar
  13. Armin Biere. CaDiCaL at the SAT Race 2019. In Marijn Heule, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B, pages 8-9. Univ.Helsinki, 2019. Google Scholar
  14. Armin Biere. Clausal congruence closure paper logs, plots and tables, June 2024. URL: https://doi.org/10.5281/zenodo.11658133.
  15. Armin Biere. Clausal congruence closure paper source code, June 2024. URL: https://doi.org/10.5281/zenodo.11652423.
  16. Armin Biere. CNF encoded hard miters from IWLS'22 paper, March 2024. URL: https://doi.org/10.5281/zenodo.10823099.
  17. Armin Biere. CNF encoded isomorphic and optimized miters from Hardware Model Checking Competition 2012 models, March 2024. URL: https://doi.org/10.5281/zenodo.10823128.
  18. Armin Biere. SAT Competition 2022 main track benchmarks, June 2024. URL: https://doi.org/10.5281/zenodo.11428010.
  19. Armin Biere. SAT Competition 2023 main track benchmarks, June 2024. URL: https://doi.org/10.5281/zenodo.11426992.
  20. 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. Univ.Helsinki, 2020. Google Scholar
  21. Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022. In Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2022 - Solver and Benchmark Descriptions, volume B-2022-1 of Department of Computer Science Series of Publications B, pages 10-11. Univ.Helsinki, 2022. Google Scholar
  22. Armin Biere, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2021 - Solver and Benchmark Descriptions, volume B-2021-1 of Department of Computer Science Report Series B, pages 10-13. Univ.Helsinki, 2021. Google Scholar
  23. Armin Biere, Mathias Fleury, and Florian Pollitt. CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT entering the SAT competition 2023. In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2023 - Solver and Benchmark Descriptions, volume B-2023-1 of Department of Computer Science Report Series B, pages 14-15. Univ.Helsinki, 2023. Google Scholar
  24. Armin Biere, Marijn Heule, Matti Järvisalo, and Norbert Manthey. Equivalence checking of HWMCC 2012 circuits. In Adrian Balint, Andon Belov, Marijn Heule, and Matti Järvisalo, editors, Proc. of SAT Competition 2013 - Solver and Benchmark Descriptions, volume B-2013-1 of Department of Computer Science Series of Publications B, page 104. Univ.Helsinki, 2013. Google Scholar
  25. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  26. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 391-435. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200992.
  27. Armin Biere, Matti Järvisalo, Daniel Le Berre, Kuldeep S. Meel, and Stefan Mengel. The SAT Practitioner’s Manifesto, September 2020. URL: https://doi.org/10.5281/zenodo.4500928.
  28. Alain Billionnet and Alain Sutter. An efficient algorithm for the 3-satisfiability problem. Oper. Res. Lett., 12(1):29-36, 1992. URL: https://doi.org/10.1016/0167-6377(92)90019-Y.
  29. Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a BDD package. In Richard C. Smith, editor, Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, Florida, USA, June 24-28, 1990, pages 40-45. IEEE Computer Society Press, 1990. URL: https://doi.org/10.1145/123186.123222.
  30. 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.
  31. 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.
  32. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 44-57. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  33. Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  34. Maciej J. Ciesielski, Cunxi Yu, Walter Brown, Duo Liu, and André Rossi. Verification of gate-level arithmetic circuits by function extraction. In Proceedings of the 52nd Annual Design Automation Conference, San Francisco, CA, USA, June 7-11, 2015, pages 52:1-52:6. ACM, 2015. URL: https://doi.org/10.1145/2744769.2744925.
  35. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 220-236. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  36. Alvaro del Val. Simplifying binary propositional theories into connected components twice as fast. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings, volume 2250 of Lecture Notes in Computer Science, pages 392-406. Springer, 2001. URL: https://doi.org/10.1007/3-540-45653-8_27.
  37. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61-75. Springer, 2005. Google Scholar
  38. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  39. Mathias Fleury and Armin Biere. Mining definitions in Kissat with Kittens. Formal Methods Syst. Des., 60(3):381-404, 2022. URL: https://doi.org/10.1007/S10703-023-00421-2.
  40. Zhaohui Fu and Sharad Malik. Extracting logic circuit structure from conjunctive normal form descriptions. In 20th International Conference on VLSI Design (VLSI Design 2007), Sixth International Conference on Embedded Systems (ICES 2007), 6-10 January 2007, Bangalore, India, pages 37-42. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/VLSID.2007.81.
  41. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008, 2008. URL: http://isaim2008.unl.edu/PAPERS/TechnicalProgram/ISAIM2008_0008_60a1f9b2fd607a61ec9e0feac3f438f8.pdf.
  42. Roman Gershman and Ofer Strichman. Cost-effective hyper-resolution for preprocessing CNF formulas. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 423-429. Springer, 2005. URL: https://doi.org/10.1007/11499107_34.
  43. Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective auxiliary variables via structured reencoding. 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 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.11.
  44. Marijn Heule and Armin Biere. Blocked clause decomposition. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings, volume 8312 of Lecture Notes in Computer Science, pages 423-438. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_29.
  45. Marijn Heule, Matti Järvisalo, and Armin Biere. Revisiting hyper binary resolution. In Carla P. Gomes and Meinolf Sellmann, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings, volume 7874 of Lecture Notes in Computer Science, pages 77-93. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38171-3_6.
  46. Marijn J. H. Heule. Proofs of unsatisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 635-668. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200998.
  47. Marijn J. H. Heule and Armin Biere. Proofs for satisfiability problems. In All about Proofs, Proofs for All (APPA), volume 55 of Math. Logic and Foundations. College Pub., 2015. Google Scholar
  48. Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason., 64(3):533-554, 2020. URL: https://doi.org/10.1007/S10817-019-09516-0.
  49. Markus Iser. Recognition and Exploitation of Gate Structure in SAT Solving. PhD thesis, Karlsruhe Institute of Technology, Germany, 2020. URL: https://nbn-resolving.org/urn:nbn:de:101:1-2020042904595660732648.
  50. Markus Iser, Felix Kutzner, and Carsten Sinz. Using gate recognition and random simulation for under-approximation and optimized branching in SAT solvers. In 29th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2017, Boston, MA, USA, November 6-8, 2017, pages 1029-1036. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/ICTAI.2017.00158.
  51. Daniela Kaufmann and Armin Biere. Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra. Int. J. Softw. Tools Technol. Transf., 25(2):133-144, 2023. URL: https://doi.org/10.1007/s10009-022-00688-6.
  52. Daniela Kaufmann, Manuel Kauers, Armin Biere, and David Cok. Arithmetic verification problems submitted to the SAT Race 2019. In Marijn Heule, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Race 2019 - Solver and Benchmark Descriptions, volume B-2019-1 of Department of Computer Science Series of Publications B, page 49. Univ.Helsinki, 2019. Google Scholar
  53. Andreas Kuehlmann and Florian Krohm. Equivalence checking using cuts and heaps. In Ellen J. Yoffa, Giovanni De Micheli, and Jan M. Rabaey, editors, Proceedings of the 34st Conference on Design Automation, Anaheim, California, USA, Anaheim Convention Center, June 9-13, 1997, pages 263-268. ACM Press, 1997. URL: https://doi.org/10.1145/266021.266090.
  54. Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, and Malay K. Ganai. Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 21(12):1377-1394, 2002. URL: https://doi.org/10.1109/TCAD.2002.804386.
  55. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Definability for model counting. Artif. Intell., 281:103229, 2020. URL: https://doi.org/10.1016/j.artint.2019.103229.
  56. Chu Min Li. Integrating equivalency reasoning into Davis-Putnam procedure. In Henry A. Kautz and Bruce W. Porter, editors, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30 - August 3, 2000, Austin, Texas, USA., pages 291-296. AAAI Press / The MIT Press, 2000. Google Scholar
  57. Robert Nieuwenhuis and Albert Oliveras. Fast congruence closure and extensions. Inf. Comput., 205(4):557-580, 2007. URL: https://doi.org/10.1016/J.IC.2006.08.009.
  58. Richard Ostrowski, Éric Grégoire, Bertrand Mazure, and Lakhdar Sais. Recovering and exploiting structural knowledge from CNF formulas. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 185-199. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_13.
  59. Tobias Philipp and Adrian Rebola-Pardo. DRAT proofs for XOR reasoning. In Loizos Michael and Antonis C. Kakas, editors, Logics in Artificial Intelligence - 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings, volume 10021 of Lecture Notes in Computer Science, pages 415-429, 2016. URL: https://doi.org/10.1007/978-3-319-48758-8_27.
  60. Jarrod A. Roy, Igor L. Markov, and Valeria Bertacco. Restoring circuit structure from SAT instances. In Proceedings of International Workshop on Logic and Synthesis (IWLS), pages 663-678, 2004. Google Scholar
  61. Amr A. R. Sayed-Ahmed, Daniel Große, Ulrich Kühne, Mathias Soeken, and Rolf Drechsler. Formal verification of integer multipliers by combining gröbner basis with logic reduction. In Luca Fanucci and Jürgen Teich, editors, 2016 Design, Automation & Test in Europe Conference & Exhibition, DATE 2016, Dresden, Germany, March 14-18, 2016, pages 1048-1053. IEEE, 2016. URL: https://ieeexplore.ieee.org/document/7459464/.
  62. Friedrich Slivovsky. Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 508-528. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_24.
  63. Gordon L. Smith, Ralph J. Bahnsen, and Harry Halliwell. Boolean comparison of hardware and flowcharts. IBM J. Res. Dev., 26(1):106-116, 1982. URL: https://doi.org/10.1147/RD.261.0106.
  64. Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 1592-1599. AAAI Press, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33011592.
  65. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in cakeml. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, volume 12652 of Lecture Notes in Computer Science, pages 223-241. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_12.
  66. Robert Endre Tarjan. A class of algorithms which require nonlinear time to maintain disjoint sets. J. Comput. Syst. Sci., 18(2):110-127, 1979. URL: https://doi.org/10.1016/0022-0000(79)90042-4.
  67. Grigorii Samuilovich Tseitin. On the complexity of derivation in propositional calculus. Studies in Mathematics and Mathematical Logic, 2:115-125, 1968. Google Scholar
  68. Allen Van Gelder and Yumi K. Tsuji. Satisfiability testing with more reasoning and less guessing. In David S. Johnson and Michael A. Trick, editors, Cliques, Coloring, and Satisfiability, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, October 11-13, 1993, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 559-586. DIMACS/AMS, 1993. Google Scholar
  69. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. 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 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  70. He-Teng Zhang, Jie-Hong R. Jiang, Luca G. Amarù, Alan Mishchenko, and Robert K. Brayton. Deep integration of circuit simulator and SAT solver. In 58th ACM/IEEE Design Automation Conference, DAC 2021, San Francisco, CA, USA, December 5-9, 2021, pages 877-882. IEEE, 2021. URL: https://doi.org/10.1109/DAC18074.2021.9586331.
  71. He-Teng Zhang, Jie-Hong R. Jiang, and Alan Mishchenko. A circuit-based SAT solver for logic synthesis. In IEEE/ACM International Conference On Computer Aided Design, ICCAD 2021, Munich, Germany, November 1-4, 2021, pages 1-6. IEEE, 2021. URL: https://doi.org/10.1109/ICCAD51958.2021.9643505.
  72. He-Teng Zhang, Jie-Hong R. Jiang, Alan Mishchenko, and Luca G. Amarù. Improved large-scale SAT sweeping. In Proc. 31st International Workshop on Logic & Synthesis, 2022. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact