Circuit Minimization with QBF-Based Exact Synthesis
Abstract
This paper presents a rewriting method for Boolean circuits that minimizes small subcircuits with exact synthesis. Individual synthesis tasks are encoded as Quantified Boolean Formulas (QBFs) that capture the full flexibility for implementing multi-output subcircuits. This is in contrast to SAT-based resynthesis, where "don't cares" are computed for an individual gate, and replacements are confined to the circuitry used exclusively by that gate. An implementation of our method achieved substantial size reductions compared to state-of-the-art methods across a wide range of benchmark circuits.
Cite
Text
Reichl et al. "Circuit Minimization with QBF-Based Exact Synthesis." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I4.25524Markdown
[Reichl et al. "Circuit Minimization with QBF-Based Exact Synthesis." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/reichl2023aaai-circuit/) doi:10.1609/AAAI.V37I4.25524BibTeX
@inproceedings{reichl2023aaai-circuit,
title = {{Circuit Minimization with QBF-Based Exact Synthesis}},
author = {Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2023},
pages = {4087-4094},
doi = {10.1609/AAAI.V37I4.25524},
url = {https://mlanthology.org/aaai/2023/reichl2023aaai-circuit/}
}