Fellner, A. (2014). Space & congruence compression of proofs [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2014.24717
Diese Arbeit präsentiert zwei Methoden zur Komprimierung von formalen Beweisen. Formale Beweise sind von großer Bedeutung in der modernen Informatik. Sie können verwendet werden um deduktive Systeme miteinander zu kombinieren. Ein Beispiel sind SAT Solver, welche ob ihrer Effektivität gerne für diverse Berechnungen verwendet werden. Ein formaler Beweis kann als Zertifikat für die Korrektheit des Ergebnisses eines SAT Solvers dienen. Des Weiteren können aus ihnen Informationen, wie etwa Interpolanten oder Unerfüllbarkeitskerne, extrahiert werden, welche zur Lösung eines Problems beitragen. Formale Beweise sind typischerweise sehr groß, siehe etwa [Boris Konev and Alexei Lisitsa. A sat attack on the erdos discrepancy conjecture. CoRR, abs/1402.2184, 2014] für einen 13 GB Beweis eines Falles der Erdos Discrepancy Conjecture. Bei solchen Beweisgrößen stoßen Computersysteme an ihre Grenzen und deswegen ist es erforderlich Beweise zu komprimieren. Unsere Arbeit präsentiert zwei Methoden zur Beweiskomprimierung. Die erste Methode entfernt Redundanzen im Kongruenzteil von SMT Beweisen. Kongruenzbeweise schließen von einer Menge an Gleichungen auf neue Gleichungen mit der Voraussetzung der vier Axiome: Reflexivität, Symmetrie, Transitivität und Kompatibilität. Beweise, die von SMT Solvern erzeugt werden, schließen oft auf neue Gleichungen aus einer unnötig großen Menge. Wir präsentieren einen neuen Kongruenzschluss-Algorithmus, der Erklärungen für gewünschte Gleichungen produziert und zeigen, dass diese Erklärungen kürzer sind als solche in Benchmark-Beweisen. Diese kürzeren Erklärungen übersetzen sich üblicherweise in kürzere Teilbeweise und einen komprimierten Gesamtbeweis. Des Weiteren beweisen wir, dass das Problem des Findens der kürzesten Erklärung NP-Vollständig ist. Die zweite Methode untersucht die Speicherplatzanforderungen von Beweisen. Beim Bearbeiten von Beweisen muss nicht der gesamte Beweis zu jeder Zeit im Speicher gelagert sein. Teilbeweise werden erst in den Speicher geladen, wenn sie benötigt werden und werden wieder aus diesem entfernt, sobald sie nicht mehr benötigt werden. In welcher Reihenfolge die Teilbeweise geladen werden, ist essentiell für die maximale Speicherplatzanforderung. Wir wollen Reihenfolgen mit niedrigen Speicherplatzanforderungen mit Hilfe von zwei neuen Algorithmen und einer Reihe an Heuristiken konstruieren.
de
This work presents two methods for compression of formal proofs. Formal proofs are of great importance to modern computer science. They can be used to combine deductive systems. For example SAT solvers are heavily used for all kinds of computations, because of their efficiency. A formal proof is a certificate of the correctness of the output of a SAT solver. Furthermore, formal proofs can provide information about the underlying problem. For example, Interpolants and unsat cores can be extracted from proofs. Typically problems tackled by automated systems are huge and so are the produced proofs. For example, [Boris Konev and Alexei Lisitsa. A sat attack on the erdos discrepancy conjecture. CoRR, abs/1402.2184, 2014] reports a 13 GB proof of one case of the Erdos Discrepancy Conjecture. With such proof sizes, computer systems reach their boundaries and that is why it is necessary to compress proofs. Our work presents two methods for proof compression. The first method removes redundancies in the congruence reasoning part of SMT proofs. Congruence reasoning deduces equalities from a set of input equations, using the four axioms reflexivity, symmetry, transitivity, and compatibility. We found that SMT solver often use an unnecessarily large set of input equations to deduce one particular equality. We present a novel explanation producing congruence closure algorithm and show that it produces shorter explanations than those we found in the benchmark proofs. By replacing long by short explanations, we construct a new, compressed proof. Furthermore, we prove that finding the shortest explanation is in general a NP-complete problem. The second method investigates the memory requirements of proofs. During processing a proof, not all parts of the proof have to be kept in memory at all times. Subproofs can be loaded into memory when needed and can be removed from memory again when they are not needed anymore. The traversal order in which subproofs are visited is essential to the maximum memory consumption during proof processing. We construct traversal orders with low memory requirements using two novel algorithms together with a collection of heuristics.
en
Additional information:
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers Zsfassung in dt. Sprache