<div class="csl-bib-body">
<div class="csl-entry">Reichl, F. X., Slivovsky, F., & Szeider, S. (2023). Circuit Minimization with Exact Synthesis: From QBF Back to SAT. In <i>IWLS 2023: 32nd International Workshop on Logic & Synthesis</i> (pp. 98–105).</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192622
-
dc.description.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.
en
dc.language.iso
en
-
dc.subject
SAT
en
dc.subject
QBF
en
dc.subject
Circuit Minimization
en
dc.title
Circuit Minimization with Exact Synthesis: From QBF Back to SAT
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.description.startpage
98
-
dc.description.endpage
105
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
IWLS 2023: 32nd International Workshop on Logic & Synthesis
-
tuw.peerreviewed
true
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-01 - Forschungsbereich Algorithms and Complexity
-
dc.description.numberOfPages
8
-
tuw.author.orcid
0000-0001-8994-1656
-
tuw.event.name
32nd International Workshop on Logic and Synthesis
en
tuw.event.startdate
05-06-2023
-
tuw.event.enddate
06-06-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Lausanne
-
tuw.event.country
CH
-
tuw.event.presenter
Reichl, Franz Xaver
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.fulltext
no Fulltext
-
item.grantfulltext
restricted
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity