On solving real-algebraic formulas in a satisfiability-modulo-theories framework

Loup, Ulrich; Sturm, Thomas; Ábrahám, Erika; Levandovskyy, Viktor

doi:37832

On solving real-algebraic formulas in a satisfiability-modulo-theories framework = Über das Lösen Reell-algebraischer Formeln in einem Satisfiability-modulo-theories Framework

Loup, Ulrich^RWTH*

2018 & 2019

Verantwortlichkeitsangabevorgelegt von Diplom-Informatiker Ulrich Loup

ImpressumAachen 2018

Umfang1 Online-Ressource (ii, 222 Seiten) : Illustrationen, Diagramme

Dissertation, RWTH Aachen University, 2018

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2019

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Ábrahám, Erika (Thesis advisor)^RWTH* ; Levandovskyy, Viktor (Thesis advisor)^RWTH* ; Sturm, Thomas (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2018-12-14

Online
DOI: 10.18154/RWTH-2018-231963
URL: http://publications.rwth-aachen.de/record/752239/files/752239.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
CAD (frei) ; Gröbner bases (frei) ; SMT solving (frei) ; cylindrical algebraic decomposition (frei) ; real algebra (frei) ; real-algebraic solving (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Reell-algebraische Formeln sind Boolesche Kombinationen polynomieller Gleichungen und Ungleichungen über dem Bereich der reellen Zahlen. Ausgestattet mit einer großer Ausdrucksstärke und einem immer noch entscheidbaren Erfüllbarkeitsproblem bilden sie eine wertvolle Sprache zur Modellierung von Problemen vieler akademischer und industrieller Bereiche. Allerdings lassen sich nicht alle reell-algebraische Formeln auch in der Praxis effizient lösen, nur einige Klassen erlauben dies. Beispielsweise können Formeln, die nur lineare Polynome enthalten, mit der sehr erfolgreichen Simplex-Methode gelöst werden. Die virtuelle Substitutionsmethode erlaubt sogar das Lösen von Formeln, die auch quadratische oder -- in manchen Fällen -- auch Polynome mit höherem Grad enthalten. Andere, nicht vollständige Methoden basieren zum Beispiel auf Interval Constraint Propagation (ICP). Damit lassen sich auch Formeln mit noch größerer Ausdrucksstärke lösen, etwa solche, die trigonometrische Funktionen beinhalten. Obwohl diese Methoden nicht immer terminieren, liefern sie dennoch oft ein verlässliches Ergebnis in einer kurzen Laufzeit. Weitere spezielle Beispiele sind Lösungsmethoden basierend auf Gröbner Basen, die nur im Kontext mit anderen Methoden zum Lösen reell-algebraischer Formeln verwendet werden können, was eine anspruchsvolle Implementierung zur Folge hat. Allgemein hat das reell-algebraische Erfüllbarkeitsproblem eine obere Zeitkomplexitätsschranke, die exponentiell in der Anzahl der Eingabevariablen ist. Darüber hinaus sind Methoden, die das allgemeine reell-algebraische Erfüllbarkeitsproblem direkt lösen sehr ineffizient im praktischen Kontext. In diesem Zusammenhang ist die Cylindrical Algebraic Decompositon (CAD)-Methode sehr bekannt. Ihr Suchraum kann sogar doppelt-exponentiell mit der Anzahl der Eingabevariablen wachsen. Demzufolge hängt ihre Praktikabilität maßgeblich von intelligenten Such-Heuristiken und Suchraum-Reduktionen ab. In dieser Arbeit werden beide Aspekte beleuchtet. Insbesondere wird die CAD-Methode zusammen mit anderen spezialisierten Methoden analysiert wie zum Beispiel Gröbner Basen. Desweiteren werden Schranken für die Eingabevariablen zur Suchraum-Reduktion verwendet, vor allem in Kombination mit ICP-Methoden. Generell behandelt diese Dissertation das Lösen allgemeiner reell-algebraischer Formeln durch eine Kombination verschiedener Methoden in einem Satisfiability-modulo-theories (SMT)-Framework: Ein SAT-Solver berechnet Teillösungen der Booleschen Struktur der reell-algebraischen Eingabeformel als eine Konjunktion reell-algebraischer Bedingungen und reell-algebraische Löser prüfen diese auf Konsistenz über den reellen Zahlen. Wenn die Teillösung dort ungültig ist, ist die Angabe eines möglichst kleinen Grundes in Form einer Teilmenge der belegten reell-algebraischen Bedingungen für die Unerfüllbarkeit gegenüber dem SAT-Solver erwünscht, da dieser dadurch möglichst große Bereich in seiner Suche abschneiden kann. Vorzugsweise minimale Gründe sind wertvoll in einem SMT-Löser. Diese Dissertation enthält eine Beschreibung und Auswertung der Berechnung solcher minimaler Gründe mittels der CAD-Methode. Zusätzlich wird der neue und interessante Ansatz der Berechnung realisierbarer Vorzeichenbedingungen nach Basu, Pollack und Roy analysiert im Hinblick auf dessen Anpassung an das SMT-Framework. Eine mögliche Implementierung wird vorgestellt.

Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations and inequalities over the domain of the real numbers. Coming with a strong expressiveness and a still decidable satisfiability problem, real-algebraic formulas are a precious modeling language in many academic, industrial and commercial areas. However, only some classes of real-algebraic formulas allow an efficient solving in practice. For instance, conjunctions of linear real-algebraic constraints can be solved with the very successful simplex method. The virtual substitution method can solve also formulas containing quadratic polynomials and, based on recent developments, also polynomials of higher degrees. Other examples are solving methods based on interval constraint propagation, which are able to deal with even more expressive formulas, e.g.~including trigonometric functions. Although those computations are not always terminating with a conclusive answer, they often lead to a reliable result in a short running time. Further special examples are solving techniques based on Gröbner bases. They can be used to solve real-algebraic formulas in combination with other techniques, making the implementation a challenging task. The general quantifier-free real-algebraic satisfiability problem, however, has a worst-case time complexity bound which is exponential in the number of input variables. Methods solving this general problem directly are often inefficient in practice. The most popular method in this respect is the cylindrical algebraic decomposition (CAD) method. Its search space can grow doubly-exponentially with the number of input variables. Thus, its practical usefulness highly depends on search heuristics and search space pruning. In this thesis, both aspects are shed light on. In particular, the CAD method is analyzed in combination with other more specialized solving methods such as Gröbner bases. Moreover, bounds to the variables are used to prune the CAD search space, especially when combining the method with interval-arithmetic techniques. This thesis tackles the solving of general quantifier-free real-algebraic formulas with a combination of different methods in a satisfiability-modulo-theories (SMT) framework: A SAT solver computes partial assignments for the Boolean structure of the real-algebraic formula and real-algebraic solvers check these assignments for consistency in the real domain. If the assignment is infeasible in the real domain, the SAT solver would profit from a small reason for this conflict in terms of a subset of the constraints corresponding to the conflicting assignment. Preferably minimal reasons are a valuable good in an SMT solver. As a main part, this thesis comprises a description and evaluation of their computation using the CAD method. In addition, the new and interesting approach for real-algebraic solving by computing realizable sign conditions is analyzed in terms of its adaptability to the SMT framework.

OpenAccess:
PDF
(additional files)