AAAI 2023technical13 citations
Circuit Minimization with QBF-Based Exact Synthesis
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
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.
BibTeX
@article{Reichl_Slivovsky_Szeider_2023, title={Circuit Minimization with QBF-Based Exact Synthesis}, volume={37}, url={https://ojs.aaai.org/index.php/AAAI/article/view/25524}, DOI={10.1609/aaai.v37i4.25524}, abstractNote={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.}, number={4}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Reichl, Franz-Xaver and Slivovsky, Friedrich and Szeider, Stefan}, year={2023}, month={Jun.}, pages={4087-4094} }