Certifying unsatisfiability in an expansion-based DQBF solver

Abstract

Mithilfe von quantifizierten booleschen Formeln (QBFs) können schwierige Probleme aus Bereichen wie der formalen Verifikation und Planung in einer kurzen und prägnanten Weise dargestellt und beschrieben werden. Jedoch ist das Erfüllbarkeitsproblem von quantifizierten booleschen Formeln (QSAT) ein PSPACE-vollständiges und somit ein schwieriges Problem. Eine weitere Generalisierung von QBF ist Dependency QBF. DQBFs erlauben für jede existenzielle Variable eine explizite Spezifikation ihrer Abhängigkeiten von universellen Variablen. Dadurch können Probleme mit DQBFs in einer noch prägnanteren Form dargestellt werden. Diese Ausdrucksstärke zieht jedoch ein höheres Komplexitätslevel mit sich. Das Erfüllbarkeitsproblem für DQBFs (DQSAT) ist ein NEXPTIME-vollständiges Problem und damit noch schwieriger zu lösen als QSAT. Durch die Komplexität dieser Probleme ist die korrekte Implementierung bzw. die Korrektheit der Ergebnisse von Solvern nicht automatisch garantiert. Um Gewissheit in die Ergebnisse von Solvern zu bekommen, generieren diese daher zusätzlich Zertifikate. Ziel der vorliegenden Arbeit ist es, die Korrektheit der Ergebnisse eines expansionsbasierten Solvers für DQBF zu verifizieren. Wir implementieren ein Tracing-Modul in Pedant, welches die Ausgabe von QRAT Beweisen für unerfüllbare QBFs ermöglicht. Dadurch kann die Unerfüllbarkeit von QBF Instanzen von QRAT-Trim verifiziert werden. Inunseren Experimenten verwenden wir unerfüllbare Instanzen aus den PCNF Tracks von QBFEVAL’19 und QBFEVAL’20. QRAT-Trim kann unter Zuhilfenahme der von Pedant erstellten Zertifikate die Unerfüllbarkeit dieser QBFs bestätigen. Das Tracing beeinflusst die Performance von Pedant nicht nennenswert.

Quantified Boolean Formulas (QBFs) can be used to represent problems in areas like formal verification and planning in a concise way. However, the satisfiability problem of quantified Boolean Formulas (QSAT) is PSPACE-complete and thus believed to be intractable in general. A further generalization of QBF is DQBF. In a dependency QBF each existential variable has an explicitly stated dependency set, which is a subset of the universal variables. The satisfiability problem of DQBFs is NEXPTIME-complete and thus believed to be even harder than QSAT. Because of the complexity of these problems the correct implementation of solvers, respectively the correctness of their output, is not easily guaranteed. In order to create certainty in solvers’ results, they need to generate certificates which can be used to verify the correctness of their results. The goal of the present work is to verify the correctness of the results of an expansion-based solver for DQBF. We implement a tracing module in Pedant which allows the generation of QRAT proofs for unsatisfiable QBFs. This allows the verification of unsatisfiable QBF instances using QRAT-Trim. We perform experiments with unsatisfiable instances from the PCNF tracks of QBFEVAL’19 and QBFEVAL’20. Using the certificates created by Pedant, QRAT-Trim can indeed confirm the unsatisfiability of these QBFs. Furthermore, tracing does not deteriorate the performance of Pedant.