Cylindrical algebraic decomposition for nonlinear arithmetic problems

Kremer, Gereon; Ábrahám, Erika (Thesis advisor); Davenport, James H. (Thesis advisor); Levandovskyy, Viktor (Thesis advisor)

Aachen (2020)
Buch, Doktorarbeit

In: Aachener Informatik-Berichte 2020-04
Seite(n)/Artikel-Nr.: 1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2020

Kurzfassung

Satisfiability modulo Theories Solving ist eine Technologie, um logisch kodierte Probleme für Anwendungen wie Verifikation, Testen oder Planungsprobleme zu lösen. Unter den in diesem Framework untersuchten Theorien sticht die nicht-lineare reelle Arithmetik heraus: Sie ist anspruchsvoll, aber noch entscheidbar, und aus mathematischer Sichthinreichend gut verstanden. Die bekannteste Möglichkeit, solche Probleme vollständig zu behandeln, ist die Methode der Zylindrisch Algebraischen Zerlegung. Wir untersuchen die Verwendung dieser Methode für Satisfiability modulo Theories sowohl theoretisch als auch experimentell. Die Methode wird typischerweise als atomarer Algorithmus verstanden, der zunächst Informationen über das Eingabeproblem sammelt und anschließend darauf basierend eine Vielzahl von Fragen über die Eingabe beantworten kann. Wir zerlegen die Methode in kleinere Teile, die dann in beliebiger Reihenfolgeausgeführt werden können, um die entscheidende Information - ob das Problem erfüllbar oder unerfüllbar ist - ableiten zu können, ohne tatsächlich alle Berechnungen vollständig durchführen zu müssen. Da die Methode häufig eine doppelt exponentielle Laufzeitaufweist, können diese Einsparungen in der Praxis erheblich sein. Wir betten diese Methode anschließend in das typische Framework für Satisfiability modulo Theories ein, bei dem die Methode der Zylindrisch Algebraischen Zerlegung eine Folge von Eingabeproblemen beantworten muss. Diese sind "ähnlich" in dem Sinne, dass üblicherweise weite Teile der Problemstellung übereinstimmen. Wir zeigen verschiedene Ansätze, um Berechnungen von vorherigen Läufen wiederzuverwenden (falls das Problem nur "erweitert" wurde) oder einzelne Berechnungen zu entfernen (falls das Problem "reduziert" wurde). Diese Varianten unterscheiden sich in Bezug auf die Menge der wiederverwendbaren Berechnungen, der Granularität der zu entfernenden Berechnungen und dem Aufwand für die Buchhaltung. Diese Einbettung wird schließlich durch mehr oder weniger bekannte Techniken aus der Computeralgebra erweitert, beispielsweise verschiedene Projektionsoperatoren, Equational Constraints oder die sogenannte Resultantenregel. Zusätzlich entwickeln wir Funktionen, die für eine effiziente Behandlung im Kontext von Satisfiability modulo Theories notwendig sind, wie Gründe für Unerfüllbarkeit, vorzeitige Terminierung oder die Erweiterung auf ganzzahlige Probleme oder Optimierungsprobleme. Anschließend wenden wir uns einem alternativen Ansatz für Satisfiability modulo Theories zu, dem Model-Constructing Satisfiability Calculus. Die Kernidee ist hierbei, die Berechnungen in der Theorie enger mit denen auf boolescher Ebene zu verzahnen, insbesondere die Konstruktion einer Belegung für Theorievariablen. Die Hauptmethode für die Theorie basiert auch hier auf der Zylindrisch Algebraischen Zerlegung, wobei wir uns in diesem Teil mehr auf das Framework konzentrieren. Wir stellen zunächst unsere Variante des Model-Constructing Satisfiability Calculus vor und diskutieren das generelle Verständnis und Unterschiede zu anderen Implementierungen. Anschließend präsentieren wir eine Reihe von Methoden für Berechnungen in der Theorie und zeigen, wie selbst eine recht naive Kombination dieser Methoden eine praktische Implementierung wesentlich verbessern kann. Zudem stellen wir fest, dass die enge Verzahnung zwischen booleschen und Theorieberechnungen neue Ansätze für notorisch schwere Probleme eröffnet, beispielsweise die Variablenordnung für Theorievariablen oder eine zielführende Kooperation zwischen booleschen und Theorieberechnungen. Zuletzt schauen wir auf den theoretischen Zusammenhang des Model-Constructing Satisfiability Calculus und anderen Beweissystemen, insbesondere dem typischen Framework für Satisfiability modulo Theories. Unter gewissen Annahmen - die bereits für sich genommen interessant sind - sind diese bezüglich ihrer Beweiskomplexität äquivalent und wir zeigen sogar einen stärkeren Zusammenhang, den wir als "algorithmische Äquivalenz" bezeichnen.