Szeider, S. (2024, July 3). Circuit Minimization with QBF and SAT-Based Exact Synthesis [Presentation]. Synthesis of Models and Systems, California, United States of America (the).
E192-01 - Forschungsbereich Algorithms and Complexity E056-13 - Fachbereich LogiCS E056-23 - Fachbereich Innovative Combinations and Applications of AI and ML (iCAIML)
In this talk, we will present new methods for re-synthesizing Boolean circuits for minimizing the number of gates. The proposed method rewrites small subcircuits with exact synthesis, where Individual synthesis tasks are encoded as Quantified Boolean Formulas (QBFs) or as SAT (propositional satisfiability) instances. A key aspect of this approach is how it handles "don't cares," which provides additional flexibility. A prototype implementation allowed us to break the record on the number of gates for some benchmark instances. Joint work with Franz-Xaver Reichl and Friedrich Slivovsky.
