Unsatisfiability Proofs in the Yices 2 SMT Solver

Abstract

Beweise der Unerfüllbarkeit für SMT-Löser zeigen nicht nur die Unerfüllbarkeit der Eingabe durch einen detaillierten Prozess, sondern auch die Gültigkeit der zugrunde liegenden Beweissuche. Diese Arbeit befasst sich mit den potenziellen Herausforderungen, die bei der Implementierung von Unerfüllbarkeitsbeweisen auftreten können, und stellt eine Pipeline zur Erstellung und Validierung des Beweiskonstruktionsrahmens vor.Konkret wird der mcSAT-Kalkül innerhalb des Yices 2 SMT-Lösers erweitert, um die Protokollierung von Beweisen zu unterstützen. Die protokollierten Beweise werden weiterverarbeitet und in das Auflösungsbeweisformat konvertiert. Um ihre Korrektheit zu beweisen, werden die Beweise mit einem externen Resolution Proof Checker validiert.Die Grenzen der gegebenen Implementierung werden diskutiert und als Möglichkeiten für Verbesserungen und weitere Arbeiten vorgestellt. Darüber hinaus werden die Ergebnisse der Implementierung anhand mehrerer Beispiele gezeigt.

Proofs of unsatisfiability for satisfiability modulo theory (SMT) solvers, apart from demonstrating input unsatisfiability through a detailed process, also demonstrate the validity of the underlying proof search. This thesis addresses some potential challenges that may arise in implementing unsatisfiability proofs and presents a pipeline for producing and validating the proof construction framework.Specifically, the mcSAT calculus within the Yices 2 SMT solver is expanded to support proof logging. The logged proofs are further processed and converted into the resolution proof format. To prove their correctness, the proofs are validated using an external resolution proof checker.The limitations of the given implementation are discussed and presented as opportunities for improvement and further work. In addition, the results of the implementation are shown through several examples.