SAT encodings: from constraint based termination analysis to circuit synthesis

Fuhs, Carsten; Giesl, Jürgen

doi:999910270864

SAT encodings: from constraint based termination analysis to circuit synthesis = SAT-Kodierungen : von constraintbasierter Terminierungsanalyse zu Schaltkreissynthese

Fuhs, Carsten (Author)

2012

VerantwortlichkeitsangabeCarsten Fuhs

ImpressumAachen : Fachgruppe Informatik, RWTH Aachen Univ. 2012

UmfangII, 188 S.

ReiheAachener Informatik-Berichte ; 2011,17

Zugl.: Aachen, Techn. Hochsch., Diss., 2012

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2011-12-21

Online
URN: urn:nbn:de:hbz:82-opus-42885
URL: https://publications.rwth-aachen.de/record/62899/files/4288.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Terminierung <Informatik> (Genormte SW) ; Verifikation (Genormte SW) ; Termersetzungssystem (Genormte SW) ; Erfüllbarkeitsproblem (Genormte SW) ; Codierung (Genormte SW) ; Logische Schaltung (Genormte SW) ; Informatik (frei) ; Schaltkreissynthese (frei) ; SAT-Codierung (frei) ; termination (frei) ; verification (frei) ; rewriting (frei) ; SAT encoding (frei) ; circuit (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: B.6.1 * I.2.2 * F.4.2 * F.3.1 * D.2.4

Kurzfassung
Terminierung ist eines der bekanntesten unentscheidbaren Probleme in der Informatik. Zugleich ist das Problem, ob ein gegebenes Programm für alle Eingaben terminiert, von solcher Bedeutung für das Gebiet der Programmverifikation, dass es jahrzehntelange Anstrengungen bei der Entwicklung von hinreichenden Kriterien für einen Terminierungsbeweis in Gang gesetzt hat. Im letzten Jahrzehnt lag der Schwerpunkt dieser Forschung auf der Automatisierung, was zur Entwicklung mehrerer mächtiger vollautomatischer Terminierungsbeweiser führte. Jedoch sind die Suchprobleme, die im Rahmen der Synthese eines erfolgreichen Terminierungsbeweises entstehen, typischerweise NP-vollständig. Um diesen algorithmischen Herausforderungen zu begegnen, hat sich in den letzten Jahren ein Vorgehen in zwei Schritten als extrem erfolgreich in der Praxis herausgestellt: Zunächst wird die entstehende Probleminstanz als Erfüllbarkeitsproblem der Aussagenlogik (SAT) kodiert, und dann wird ein moderner SAT-Solver auf dieser SAT-Instanz aufgerufen. Die durch den SAT-Solver gefundene Lösung kommt dann im Terminierungsbeweis zum Einsatz. Auch wenn dieser Ansatz im schlimmsten Fall wegen der NP-Vollständigkeit von SAT immer noch zu aufwändig ist, so hat er doch die Effizienz auf Probleminstanzen aus der Praxis um Größenordnungen verbessert. Zugleich hat der Ansatz auch neue automatisierte Techniken ermöglicht, die zuvor außer Reichweite lagen. Die Beiträge dieser Dissertation betreffen SAT-basierte Automatisierungen sowohl für mehrere bestehende Terminierungstechniken als auch für neue Techniken, die wir im Rahmen des Dependency-Pair-Frameworks für die Terminierungsanalyse von Termersetzung entwickelt haben. Der Nutzen von SAT-Kodierungen geht über das Feld der Terminierungsanalyse hinaus. Wir haben den für Terminierungstechniken eingesetzten Ansatz in den - auf den ersten Blick - eher anders gearteten Anwendungsbereich der Schaltkreissynthese übertragen, was uns ermöglicht hat, eine beweisbar optimale Implementierung für einen Teil des Advanced Encryption Standard zu erhalten. Die Beiträge dieser Dissertation sind in unserem vollautomatischen Terminierungsbeweiser AProVE implementiert. Die Bedeutung unserer Ergebnisse wird auch dadurch deutlich, dass AProVE in den jährlichen International Termination Competitions von 2007 bis 2011 die besten Ergebnisse erreichen konnte. In diesen Wettbewerben versuchen die führenden automatischen Tools für Terminierungsanalyse die Terminierung von Programmen aus verschiedenen Bereichen der Informatik zu beweisen oder zu widerlegen.

Termination is one of the most prominent undecidable problems in computer science. At the same time, the problem whether a given program terminates for all inputs is sufficiently important for the area of program verification to spur decades-long efforts in developing sufficient criteria for concluding termination. In the last decade, the focus of this research has been on automation, giving rise to several powerful fully automatic termination provers. However, the search problems that arise during the synthesis of a successful termination proof are typically NP-complete. To tackle these algorithmic challenges, over the last years a two-stage process has turned out to be extremely successful in practice: First encode the arising problem instance to the satisfiability problem of propositional logic (SAT), and then invoke a state-of-the-art SAT solver on this SAT instance. The solution found by the SAT solver is then used in the termination proof. While in the worst case still prohibitive due to NP-completeness of SAT, this approach has increased performance on practical problem instances for existing termination techniques by orders of magnitude. At the same time, the approach has also made new automated techniques possible that were out of reach before. This thesis contributes efficient SAT-based automation both for several existing termination techniques and also for new techniques that we have developed in the dependency pair framework for termination analysis of term rewriting. The usefulness of SAT encodings goes beyond the field of termination analysis. We have transferred the approach used for termination techniques to the - at first glance - quite distinct application domain of circuit synthesis, allowing us to obtain a provably optimal implementation of a part of the Advanced Encryption Standard. The contributions of this thesis are implemented within our fully automated termination prover AProVE. The significance of our results is demonstrated also by AProVE reaching the highest scores in the annual International Termination Competitions of 2007 - 2011. At these competitions, the leading automated termination analysis tools try to prove or disprove termination of programs originating from various areas of computer science.

Fulltext:
PDF