License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2022.67
URN: urn:nbn:de:0030-drops-168659
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16865/
Go to the corresponding LIPIcs Volume Portal

Kulikov, Alexander S. ; Pechenev, Danila ; Slezkin, Nikita

SAT-Based Circuit Local Improvement

pdf-format:
LIPIcs-MFCS-2022-67.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{kulikov_et_al:LIPIcs.MFCS.2022.67,
  author =	{Kulikov, Alexander S. and Pechenev, Danila and Slezkin, Nikita},
  title =	{{SAT-Based Circuit Local Improvement}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{67:1--67:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16865},
  URN =		{urn:nbn:de:0030-drops-168659},
  doi =		{10.4230/LIPIcs.MFCS.2022.67},
  annote =	{Keywords: circuits, algorithms, complexity theory, SAT, SAT solvers, heuristics}
}

Keywords: circuits, algorithms, complexity theory, SAT, SAT solvers, heuristics
Collection: 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Issue Date: 2022
Date of publication: 22.08.2022
Supplementary Material: Software (Source Code): https://github.com/alexanderskulikov/circuit_improvement

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI