Efficient Reasoning with Quantifiers and Theories

Abstract

Automatische Beweiser wie SAT- und SMT-Solver, sowie Beweiser für Prädikatenlogikerster Stufe, werden immer wichtigere Komponenten in zahlreichen Anwendungen, vorallem im Bereich der formalen Methoden, wie beispielsweise in Software zur automatisierten deduktiven Verifikation, Programmsynthese und der Sicherheitsanalyse von Programmen. Insbesondere im Bereich der formalen Methoden hängt der Automati-sierungsgrad entscheidend von der Effizienz der zugrunde liegenden Beweiser bei der Suche nach Beweisen und/oder Gegenbeispielen für die zu lösende Aufgabe ab. Das Zielder vorliegenden Dissertation ist es, motiviert durch die Anwendungen im Bereich der automatischen Analyse von Programmen, die Effizienz der automatisierten Beweiser in verschiedenen Bereichen zu verbessern.Der erste Teil der Arbeit beschäftigt sich mit der Optimierung von auf Saturierungbasierenden Theorembeweisern für Prädikatenlogik erster Stufe. Beweiser dieser Art verwenden Inferenzregeln, um schrittweise Konsequenzen aus der Eingabe herzuleiten.Eine besondere Herausforderung ist dabei die enorme Menge an möglichen Konsequenzen, die die Suche nach Beweisen empfindlich verlangsamt. Einen gängigen Ansatz zur Verbesserung dieses Problems bieten sogenannte Vereinfachungsregeln: spezielle Inferenzregeln, deren Verwendung die Anzahl redundanter Klauseln reduziert oder zumindest nicht weiter erhöht.Wir führen eine neue Inferenzregel namens Subsumption Demodulation ein, um das Erkennen von Redundanzen im Zusammenhang mit bedingten Gleichungen in Beweisern,die auf dem Superpositionskalkül basieren, zu verbessern. Wir zeigen, dass Subsumption Demodulation eine Vereinfachungsregel ist, die keine fundamentalen Änderungen am zugrunde liegenden Superpositionskalkül erfordert. Durch Erweiterung um einen neuen Klauselindex und Anpassung der Multiliteral-Matching-Komponente konnten wir Subsumption Demodulation effizient in dem Theorembeweiser Vampire implementieren.Unsere Experimente zeigen, dass Vampire mit Hilfe der in dieser Dissertation beschriebenen Änderungen mehrere neue Probleme aus den Benchmark-Sammlungen TPTP und SMT-LIB lösen kann, die bisher von modernen Beweisern nicht gelöst werden konnten. Darüber hinaus wenden wir uns der Subsumption-Regel zu, die eine der wichtigsten Beweisregeln in der Praxis ist. Es kommt häufig vor, dass während der Beweissuche Millionen von potenziellen Anwendungen von Subsumption geprüft werden, weshalb eine effiziente Implementierung erforderlich ist. Im Gegensatz zu Subsumption in der Aussagenlogik, die von SAT-Solvern verwendet wird und ausgefeilte Algorithmen mit polynomieller Laufzeit erlaubt, erfordert Subsumption in der Prädikatenlogik erster Stufe die Lösung eines NP-vollständigen Entscheidungsproblems. Dadurch ist die effiziente Nutzung von Subsumption in der Prädikatenlogik erster Stufe eine große praktische Herausforderung. In der vorliegenden Arbeit zeigen wir, dass die Integration eines dedizierten SAT-Solvers eine gute Möglichkeit zur effizienten Implementierung von Subsumption und verwandter Regeln bietet und damit die Skalierbarkeit des Theorembeweisens in Logik erster Stufe für Anwendungen formaler Methoden verbessert. Unsere experimentellen Ergebnisse zeigen, dass wir durch die Verwendung eines maßgeschneiderten SAT-Solvers innerhalb von Vampire einen großen Geschwindigkeitszuwachs in aktuellen Benchmarks erzielen.Im zweiten Teil der Dissertation betrachten wir Bitvektoren im Kontext von SMT-Solvern.Wir stellen PolySAT vor, ein Entscheidungsverfahren auf Wortebene, das bit-präzisesSchließen über polynomiale Arithmetik mit Operationen über Bitvektoren großer Länge erlaubt. Der PolySAT-Kalkül erweitert konfliktgesteuertes Klausel lernen modulo Theorien um zwei Schlüsselkomponenten: (i) ein Bitvektor-Plugin für den Gleichheitsgraphen,und (ii) einen Theorielöser für Bitvektor-Arithmetik mit nicht-linearen Polynomen. PolySAT implementiert spezielle Verfahren zur Extraktion von Bitvektor-Intervallen aus polynomialen Ungleichungen. Zur Konfliktanalyse und -resolution generiert PolySATon demand Lemmas über nicht-linearer Bitvektor-Arithmetik. PolySAT wurde in denSMT-Solver Z3 integriert und hat potenzielle Anwendungen in der Modellprüfung undder Verifikation von Smart Contracts, wo die üblicherweise verwendete Methode desbit-blasting auf Multiplikationen/Divisionen an ihre Grenzen stößt.

Automated reasoners, such as SAT and SMT solvers as well as first-order theorem provers, are becoming the backbones of applications of formal methods, for example in automating deductive verification, program synthesis, and security analysis. Automation in these formal methods domains crucially depends on the efficiency of the underlying reasoners towards finding proofs and/or counter examples of the task to be enforced. The goal of this thesis is to improve efficiency of automated reasoning on different levels, inspired by automation of formal methods.The first part of the thesis deals with improving efficiency of saturation-based first-order theorem proving. Such theorem provers use dedicated proof rules to keep proof search manageable. Inspired by applications in program verification, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus and hence can be efficiently integrated in superposition provers. We implement subsumption demodulation in the theorem prover Vampire, by extending Vampire with a new clause index and adapting its multi-literal matching component. Our experiments,using the TPTP and SMT-LIB benchmark repositories, show that subsumption demodulation in Vampire can solve several new problems that previously could not be solved by state-of-the-art reasoners.Next, we turn our attention to subsumption, which is one of the most important proofrules in practice. It is common that millions of subsumption checks are performedduring proof search, necessitating efficient implementations. However, in contrast topropositional subsumption as used by SAT solvers and implemented using sophisticatedpolynomial algorithms, first-order subsumption in first-order theorem provers involvesNP-complete search queries, turning the efficient use of first-order subsumption intoa huge practical burden. In this thesis, we argue that integration of a dedicated SATsolver provides a remedy towards efficient implementation of first-order subsumptionand related rules, and thus further increasing scalability of first-order theorem provingtowards applications of formal methods. Our experimental results demonstrate that,by using a tailored SAT solver within first-order reasoning, we gain a large speed-up instate-of-the-art benchmarks.In the second part of the thesis, we examine bit-vector reasoning within SMT solving.We introduce PolySAT, a word-level decision procedure supporting bit-precise SMTreasoning over polynomial arithmetic with large bit-vector operations. The PolySATcalculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.