A Tiny tweak to proof generation in miniSat-based SAT solvers & a complete and efficient DRAT proof checker

Abstract

Das klauselbasierte Beweisformat DRAT ist der De-Facto-Standard, um Unerfüllbarkeitsergebnisse von SAT-Gleichungslösern zu verifizieren. DRAT-Beweise bestehen aus Lemmas, die Klauseln hinzufügen, und Klauseleliminierungen. Moderne DRAT-Beweisprüfer ignorieren Eliminierungsinstruktionen von sogenannten Unit-Klauseln, was bedeutet, dass sich die Semantik der Beweisprüfer von der DRAT-Spezifikation unterscheidet; infolgedessen können sie manche, von SAT-Lösern verwendete Vereinfachungstechniken, die Unit-Klauseln eliminieren unter Umständen nicht verifizieren. Moderne SAT-Löser generieren Beweise die von diesen DRAT-Prüfern akzeptiert werden, jedoch bezüglich der DRAT-Spezifikation inkorrekt sind, da sie Eliminierungsinstruktionen enthalten, die nicht-redundante Informationen löschen. Wir schlagen Korrekturen für prämierte SAT-Löser vor, wodurch diese in der Lage sind, Beweise ohne ebenjene kontraproduktiven Eliminierungen zu generieren, die ergo im Sinne der Spezifikation korrekt sind. Dennoch können Unit-Eliminierungen in Beweisen in Anbetracht der Verwendung von fortgeschrittenen Vereinfachungstechniken wohl kaum ausgeschlossen werden, sofern der Löseaufwand nicht darunter leiden soll. Die Durchführung von Unit-Eliminierungen in Beweisprüfern kann viel Rechenzeit beanspruchen. Wir haben den ersten wettbewerbsfähigen Prüfer implementiert, der Unit-Eliminierungen berücksichtigt and präsentieren unsere Versuchsergebnisse, die darauf hindeuten, dass der Rechenaufwand für das Überprüfen eines durchschnittlichen Beweises mit oder ohne Unit-Eliminierungen gleich ist. Weiters führen wir das SICK-Format ein, das, vergleichsweise kleine und effizient überprüfbare Gegenbeispiele zu DRAT-Beweisen beschreibt. Indem wir diese Gegenbeispiele mit einem unabhängigen Programm überprüfen, stärken wir das Vertrauen in die Stichhaltigkeit der Inkorrektheits-Ergebnisse. Außerdem kann diese Technik von Nutzen sein um Fehler in (der Beweisgenerierung von) SAT-Lösern und Prüfern zu finden.

Clausal proof format DRAT is the de facto standard way to certify SAT solvers' unsatisfiability results. DRAT proofs consist of lemmas (clause introductions) and clause deletions. State-of-the-art DRAT proof checkers ignore deletions of unit clauses, which means that they are checking against a proof system that differs from the specification of DRAT and they may not be able to verify inprocessing techniques that use unit deletions. State-of-the-art SAT solvers produce proofs that are accepted by those DRAT checkers, but are incorrect under the DRAT specification, because they contain spurious deletions of unit clauses. We present patches for award-winning SAT solvers to produce proofs without those deletions that are thus correct with respect to the specification. However, handling unit deletions is still desirable, as they can be a byproduct of advanced inprocessing techniques in a solver that is hard to avoid without extra costs. Performing unit deletions in a proof checker can be computationally expensive. We implemented the first competitive checker that honors unit deletions and provide experimental results suggesting that, on average, checking costs are the same as when not applying unit deletions. As it is also expensive to determine the incorrectness of a proof, we introduce the SICK format which describes small and efficiently checkable certificates of the incorrectness of a DRAT proof. By checking this independently, we are able to increase trust in our incorrectness results. Additionally it can be useful when debugging solvers and checkers.