Document Open Access Logo

SAT-Based Circuit Local Improvement

Authors Alexander S. Kulikov , Danila Pechenev , Nikita Slezkin

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.67.pdf
  • Filesize: 0.73 MB
  • 15 pages

Document Identifiers

Author Details

Alexander S. Kulikov
  • Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences, Russia
  • St. Petersburg State University, Russia
Danila Pechenev
  • St. Petersburg State University, Russia
Nikita Slezkin
  • St. Petersburg State University, Russia

Funding

  • Kulikov, Alexander S.: Supported by Russian Science Foundation (18-71-10042).

Acknowledgements

We are grateful to anonymous reviewers for many useful suggestions.

Cite AsGet BibTex

Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin. SAT-Based Circuit Local Improvement. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.67

Abstract

Finding exact circuit size is notoriously hard. Whereas modern computers and algorithmic techniques allow to find a circuit of size seven in the blink of an eye, it may take more than a week to search for a circuit of size thirteen. One of the reasons of this behavior is that the search space is enormous: the number of circuits of size s is s^Θ(s), the number of Boolean functions on n variables is 2^(2ⁿ). In this paper, we explore the following natural heuristic idea for decreasing the size of a given circuit: go through all its subcircuits of moderate size and check whether any of them can be improved by reducing to SAT. This may be viewed as a local search approach: we search for a smaller circuit in a ball around a given circuit. Through this approach, we prove new upper bounds on the circuit size of various symmetric functions. We also demonstrate that some upper bounds that were proved by hand decades ago, can nowadays be found automatically in a few seconds.

Subject Classification

ACM Subject Classification
  • Theory of computation → Circuit complexity
Keywords
  • circuits
  • algorithms
  • complexity theory
  • SAT
  • SAT solvers
  • heuristics

Metrics

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

Related Versions

Supplementary Materials

References

  1. URL: https://github.com/berkeley-abc/abc.
  2. Joshua Brakensiek, Marijn Heule, John Mackey, and David Narváez. The resolution of Keller’s conjecture. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 48-65. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_4.
  3. URL: https://github.com/alexanderskulikov/circuit_improvement.
  4. Evgeny Demenkov, Arist Kojevnikov, Alexander S. Kulikov, and Grigory Yaroslavtsev. New upper bounds on the boolean circuit complexity of symmetric functions. Inf. Process. Lett., 110(7):264-267, 2010. URL: https://doi.org/10.1016/j.ipl.2010.01.007.
  5. Paul E. Dunne. Techniques for the analysis of monotone Boolean networks. PhD thesis, University of Warwick, 1984. Google Scholar
  6. Johannes Klaus Fichte, Neha Lodha, and Stefan Szeider. Sat-based local improvement for finding tree decompositions of small width. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 401-411. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_25.
  7. Magnus Gausdal Find, Alexander Golovnev, Edward A. Hirsch, and Alexander S. Kulikov. A better-than-3n lower bound for the circuit complexity of an explicit function. In Irit Dinur, editor, IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9-11 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA, pages 89-98. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/FOCS.2016.19.
  8. Winston Haaswijk, Alan Mishchenko, Mathias Soeken, and Giovanni De Micheli. SAT based exact synthesis using DAG topology families. In Proceedings of the 55th Annual Design Automation Conference, DAC 2018, San Francisco, CA, USA, June 24-29, 2018, pages 53:1-53:6. ACM, 2018. URL: https://doi.org/10.1145/3195970.3196111.
  9. Alexey Ignatiev, António Morgado, and João Marques-Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  10. URL: http://www-cs-faculty.stanford.edu/~knuth/programs.html.
  11. Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 0: Introduction to Combinatorial Algorithms and Boolean Functions (Art of Computer Programming). Addison-Wesley Professional, 1 edition, 2008. Google Scholar
  12. Donald E. Knuth. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley Professional, 1st edition, 2015. Google Scholar
  13. Arist Kojevnikov, Alexander S. Kulikov, and Grigory Yaroslavtsev. Finding efficient circuits using SAT-solvers. 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 32-44. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_5.
  14. Alexander S. Kulikov. Improving circuit size upper bounds using sat-solvers. In Jan Madsen and Ayse K. Coskun, editors, 2018 Design, Automation & Test in Europe Conference & Exhibition, DATE 2018, Dresden, Germany, March 19-23, 2018, pages 305-308. IEEE, 2018. URL: https://doi.org/10.23919/DATE.2018.8342026.
  15. Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin. Sat-based circuit local improvement. CoRR, abs/2102.12579, 2021. URL: http://arxiv.org/abs/2102.12579.
  16. Neha Lodha, Sebastian Ordyniak, and Stefan Szeider. A SAT approach to branchwidth. ACM Trans. Comput. Log., 20(3):15:1-15:24, 2019. URL: https://doi.org/10.1145/3326159.
  17. Oleg Lupanov. A method of circuit synthesis. Izvestiya VUZov, Radiofizika, 1:120-140, 1959. Google Scholar
  18. David E. Muller. Complexity in electronic switching circuits. IRE Transactions on Electronic Computers, EC-5:15-19, 1956. Google Scholar
  19. URL: https://pygraphviz.github.io/.
  20. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Maxsat-based postprocessing for treedepth. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 478-495. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_28.
  21. Vaidyanathan Peruvemba Ramaswamy and Stefan Szeider. Turbocharging treewidth-bounded bayesian network structure learning. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3895-3903. AAAI Press, 2021. URL: https://ojs.aaai.org/index.php/AAAI/article/view/16508.
  22. André Schidler and Stefan Szeider. Sat-based decision tree learning for large data sets. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3904-3912. AAAI Press, 2021. URL: https://ojs.aaai.org/index.php/AAAI/article/view/16509.
  23. Igor Sergeev. On monotone circuit complexity of threshold boolean functions. Diskretnaya Matematika, 32:81-109, 2020. URL: https://doi.org/10.4213/dm1547.
  24. Mathias Soeken, Heinz Riener, Winston Haaswijk, Eleonora Testa, Bruno Schmitt, Giulia Meuli, Fereshte Mozafari, and Giovanni De Micheli. The EPFL logic synthesis libraries, November 2019. arXiv:1805.05121v2. Google Scholar
  25. Larry J. Stockmeyer. On the combinational complexity of certain symmetric boolean functions. Mathematical Systems Theory, 10:323-336, 1977. URL: https://doi.org/10.1007/BF01683282.
  26. Ingo Wegener. The complexity of Boolean functions. Wiley-Teubner, 1987. URL: http://ls2-www.cs.uni-dortmund.de/monographs/bluebook/.
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