Leveraging Dominators for Preprocessing QBF

Many CAD for VLSI problems can be naturally encoded as Quantified Boolean Formulas (QBFs) and solved with QBF solvers. Furthermore, such problems often contain circuit-based information that is lost during the translation to Conjunctive Normal Form (CNF), the format accepted by most modern solvers. In this work, a novel preprocessing framework for circuit-based QBF problems is presented. It leverages structural circuit dominators to reduce the problem size and expedite the solving process. The authors' circuit-based QBF preprocessor PReDom recursively reduces dominated sub-circuits to return a simpler but equisatisfiable QBF instance. A rigorous proof is given for eliminating sub-circuits dominated by single outputs, irrespective of input quantifiers.