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 circuitbased 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. Our circuit-based QBF preprocessor PReDom recursively reduces dominated subcircuits to return a simpler but equisatisfiable QBF instance. A rigorous proof is given for eliminating subcircuits dominated by single outputs, irrespective of input quantifiers. Experimental results are presented for circuit diameter computation problems. With preprocessing times of at most five seconds using PReDom, three state-of-the-art QBF solvers can solve 27% to 45% of our problem instances, compared to none wi...

• Type: Conference
• Year: 2010
• Where: DATE
• Authors: Hratch Mangassarian, Bao Le, Alexandra Goultiaeva, Andreas G. Veneris, Fahiem Bacchus
• Keywords: Circuit-based Qbf Problems, DATE 2010, Hardware, Preprocessing, Qbf Solvers