Finding Small Unsatisfiable Cores to Prove Unsatisfiability of QBFs.
Yannet Interian, Gabriel Corvera, Bart Selman, Ryan Williams · 2006
In the past few years, we have seen significant progress in the area of Boolean satisfiability (SAT) solving and its applications. More recently, new e#orts have focused on developing solvers for Quantified Boolean Formulas (QBFs). Recent QBF evaluation results show that developing practical QBF solvers is more challenging than one might expect. Even relatively small QBF problems are sometimes beyond the reach of current QBF solvers. We present a new approach for solving unsatisfiable two-alternation QBFs. Our approach is able to solve hard random QBF formulas that current algorithms are not able to handle.