Circuit Minimization with QBF and SAT-Based Exact Synthesis

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.