Circuit Minimization with QBF and SAT-Based Exact Synthesis

Explore new methods for re-synthesizing Boolean circuits to minimize gate count in this 44-minute talk by Stefan Szeider from TU Wien. Delve into the proposed approach that rewrites small subcircuits using exact synthesis, with synthesis tasks encoded as Quantified Boolean Formulas (QBFs) or SAT instances. Understand the crucial role of handling "don't cares" in providing additional flexibility. Learn about the prototype implementation that broke records for gate count in benchmark instances. Gain insights into this joint work with Franz-Xaver Reichl and Friedrich Slivovsky, presented as part of the Synthesis of Models and Systems series at the Simons Institute.