2026-07-20T05:24:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16865 2024-03-06T10:58:32Z ddc:004 open_access

SAT-Based Circuit Local Improvement Kulikov, Alexander S. Pechenev, Danila Slezkin, Nikita circuits algorithms complexity theory SAT SAT solvers heuristics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander S. Kulikov and Danila Pechenev and Nikita Slezkin 2022 Is Part Of LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2022.67 urn:nbn:de:0030-drops-168659 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.67 eng https://creativecommons.org/licenses/by/4.0/legalcode