FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas

To witness the correctness of unsatisfiablility results of SAT solvers, the powerful resolution asymmetric tautology (RAT) proof system has been introduced, for which efficient proof checkers are available. To harness the power of recent SAT technology for solving quantified Boolean formulas (QBFs), the extension of SAT with quantifiers over the Boolean variables, we introduce the proof system ∀-Exp+RAT. With this proof system, it becomes possible to use modern SAT solvers for expansion-based QBF solving, one of the most successful QBF solving paradigms. So far, expansion-based QBF solving relied on the resolution-based ∀-Exp+Res proof system which is less powerful than ∀-Exp+RAT.
Based on the ∀-Exp+RAT proof system, we present the new certification framework FERAT for generating and checking ∀-Exp+RAT certificates. In a detailed evaluation, we show that with the FERAT pipeline, more formula instances can be certified than with the previous FERP pipeline which relies on the ∀-Exp+Res proof system.