h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Cylindrical algebraic decomposition for nonlinear arithmetic problems



VerantwortlichkeitsangabeGereon Kremer

ImpressumAachen 2020

Umfang1 Online-Ressource (204 Seiten) : Illustrationen, Diagramme

ReiheAachener Informatik-Berichte ; 2020-04


Dissertation, RWTH Aachen University, 2020

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
; ;

Tag der mündlichen Prüfung/Habilitation
2020-03-12

Online
DOI: 10.18154/RWTH-2020-05913
URL: https://publications.rwth-aachen.de/record/792185/files/792185.pdf

Einrichtungen

  1. Lehr- und Forschungsgebiet Theorie Hybrider Systeme (123420)
  2. Fachgruppe Informatik (120000)

Inhaltliche Beschreibung (Schlagwörter)
cylindrical algebraic decomposition (frei) ; model-constructing satisfiability calculus (frei) ; nonlineararithmetic (frei) ; satisfiability modulo theories (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

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.

Satisfiability modulo theories solving is a technology to solve logically encoded problems for many applications like verification, testing, or planning. Among the many theories that are considered within this logical framework, nonlinear real arithmetic stands out as particularly challenging, yet decidable and sufficiently well understood from a mathematical perspective. The most prominent approach that can decide upon nonlinear real questions in a complete way is the cylindrical algebraic decomposition method. We explore the usage of the cylindrical algebraic decomposition method for satisfiability modulo theories solving, both theoretically and experimentally. This method is commonly understood as an almost atomic procedure that gathers information about an algebraic problem and then allows to answer all kinds of questions about this algebraic problem afterward. We essentially break up this method into smaller components that we can then process in varying order to derive the particular piece of information - whether the problem is satisfiable or unsatisfiable - allowing to avoid some amount of computations. As this method often exhibits doubly exponential running time, these savings can be very significant in practice. We furthermore embed this method in the regular satisfiability modulo theories framework where the cylindrical algebraic method is faced with a sequence of problems that are “related” in the sense that they usually share large parts of their problem statements. We devise different approaches to retain information from a previous run so that it can be reused when the problem is only “extended” as well as purging now obsolete information if the problem is “reduced”. These variants change in how much information can be reused, the granularity of the information that is removed, and how much bookkeeping needs to be done. This integration is then enhanced with techniques that are more or less well-known in the computer algebra community, for example, different projection operators, equational constraints, or employing the so-called resultant rule. Furthermore, we present novel features necessary for an efficient embedding in the satisfiability modulo theories frame-work like infeasible subset computations and early termination as well as extensions to integer problems and optimization problems. We then turn to an alternative approach to satisfiability modulo theories solving that is commonly called model-constructing satisfiability calculus. The core idea of this framework is to integrate the theory reasoning, in particular the construction of a theory model, tightly with the Boolean reasoning. The most popular theory reasoning engine is again based on the cylindrical algebraic decomposition method, though we focus on the overall framework here. We start with our own variant of the model-constructing satisfiability calculus and discuss some general insights and changes compared to current implementations. We then proceed to present a whole series of reasoning engines for arithmetic problems and show how a proper (though still naive) combination of those serves to significantly improve a practical solver. We also show how the tight integration into the Boolean reasoning allows for novel strategies for notoriously hard problems like the theory variable ordering or expedient cooperation between the Boolean and the theory reasoning. Finally, we consider the theoretical relation of the model-constructing satisfiability calculus to other proof systems, in particular, the aforementioned regular satisfiability modulo theories solving. Under certain assumptions - that turn out to be instructive in and of themselves - we show that they are equivalent with respect to their proof complexity and even establish what we call “algorithmic equivalency” afterward.

OpenAccess:
Download fulltext PDF
(additional files)

Dokumenttyp
Dissertation / PhD Thesis/Book

Format
online

Sprache
English

Externe Identnummern
HBZ: HT020476141

Interne Identnummern
RWTH-2020-05913
Datensatz-ID: 792185

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Document types > Books > Books
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
123420

 Record created 2020-06-04, last modified 2023-04-11


OpenAccess:
Download fulltext PDF
(additional files)
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)