Reichl, F. X., Slivovsky, F., & Szeider, S. (2023). Circuit Minimization with Exact Synthesis: From QBF Back to SAT. In IWLS 2023: 32nd International Workshop on Logic & Synthesis (pp. 98–105).
E192-01 - Forschungsbereich Algorithms and Complexity
-
Published in:
IWLS 2023: 32nd International Workshop on Logic & Synthesis
-
Date (published):
2023
-
Event name:
32nd International Workshop on Logic and Synthesis
en
Event date:
5-Jun-2023 - 6-Jun-2023
-
Event place:
Lausanne, Switzerland
-
Number of Pages:
8
-
Peer reviewed:
Yes
-
Keywords:
SAT; QBF; Circuit Minimization
en
Abstract:
The exact synthesis problem is to find a smallest (or shallowest) circuit matching a given specification. SAT-based exact synthesis is currently limited to circuits of about 10 gates, but can be used to minimize larger circuits by optimally resynthesizing small subcircuits. In this setting, subcircuits can often be replaced by non-equivalent circuits due to “don’t cares”. Quantified Boolean Formulas (QBFs) succinctly encode local resynthesis tasks subject to don’t cares, and QBF solvers can be used to solve the resulting instances. This paper describes two refinements of this approach. First, for subcircuits with few inputs and outputs, it is feasible to compute a Boolean relation that completely characterizes the input-output behaviour of the subcircuit under don’t cares. This enables the use of a SAT encoding instead of a QBF encoding, leading to significantly reduced running times when applied to functions from the IWLS22 and IWLS23 competitions. Second, we describe circuit partitioning techniques in which don’t cares for a subcircuit are captured only with respect to an enclosing window, rather than the entire circuit. This successfully enables the application of exact synthesis to some of the largest circuits in the EPFL suite.
