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

Abstract

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.