Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
SAT-Based Circuit Local Improvement. / Куликов, Александр Сергеевич; Печенев, Данила Евгеньевич; Слезкин, Никита Евгеньевич.
47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022. ed. / Stefan Szeider; Robert Ganian; Alexandra Silva. Dagstuhl, Germany : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. 68 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 241).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
}
TY - GEN
T1 - SAT-Based Circuit Local Improvement
AU - Куликов, Александр Сергеевич
AU - Печенев, Данила Евгеньевич
AU - Слезкин, Никита Евгеньевич
N1 - Publisher Copyright: © 2022 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. All rights reserved.
PY - 2022/8/1
Y1 - 2022/8/1
N2 - 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 22n. 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.
AB - 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 22n. 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.
KW - algorithms
KW - circuits
KW - complexity theory
KW - heuristics
KW - SAT
KW - SAT solvers
UR - http://www.scopus.com/inward/record.url?scp=85137585280&partnerID=8YFLogxK
UR - http://arxiv.org/abs/2102.12579
UR - https://www.mendeley.com/catalogue/5f707b96-868e-3893-a32a-2516938b5134/
U2 - 10.4230/LIPIcs.MFCS.2022.67
DO - 10.4230/LIPIcs.MFCS.2022.67
M3 - Conference contribution
SN - 9783959772563
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022
A2 - Szeider, Stefan
A2 - Ganian, Robert
A2 - Silva, Alexandra
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
CY - Dagstuhl, Germany
Y2 - 22 August 2022 through 26 August 2022
ER -
ID: 98049855