guest ::
Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic
2025
Dissertation, RWTH Aachen University, 2025
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
Genehmigende Fakultät
Fak09
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2025-11-12
Online
DOI: 10.18154/RWTH-2025-09926
URL: http://publications.rwth-aachen.de/record/1022295/files/1022295.pdf
Einrichtungen
Projekte
Inhaltliche Beschreibung (Schlagwörter)
cylindrical algebraic decomposition (frei) ; non-linear real arithmetic (frei) ; quantifier elimination (frei) ; real algebra (frei) ; satisfiability modulo theories (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Die Theorie erster Ordnung der reellen Zahlen bietet eine ausdrucksstarke Sprache mit einer Vielzahl von Anwendungsmöglichkeiten. Die Methode der zylindrischen algebraischen Zerlegung ist ein leistungsfähiges Werkzeug aus der reellen Algebra zur Beantwortung verschiedener Arten von Problemen im Zusammenhang mit der Theorie der reellen Zahlen, darunter die Erfüllbarkeit von quantorenfreien Formeln, die Gültigkeit von Sätzen und die Eliminierung von Quantoren. Sie zerlegt den reellen Raum in endlich viele Teilmengen, in denen bestimmte Eigenschaften der Polynome aus der Eingabe-Formel invariant sind. Die sich daraus ergebende Zerlegung wird dann verwendet, um auf die Eigenschaften der Eingabe-Formel zu schließen. Trotz seiner doppelt exponentiellen Komplexitätsgrenze ist die Methode der zylindrischen algebraischen Zerlegung bis heute die Grundlage aller Algorithmen, die in modernen Werkzeugen implementiert sind. Satisfiability-modulo-theories Solving ist eine Technik zur Überprüfung der Erfüllbarkeit von quantorenfreien Formeln der Logik erster Ordnung über eine oder mehrere Theorien. Moderne Solver unterstützen eine breite Palette von Theorien und werden bei realen Problemen eingesetzt. Im letzten Jahrzehnt wurden diese Solver so erweitert, dass sie auch reelle arithmetische Formeln unterstützen, die auf Ideen aus der zylindrischen algebraischen Zerlegung basieren. Anstatt eine vollständige Zerlegung zu berechnen, folgen diese Anpassungen einem explorationsgeleiteten Ansatz: Durch das Raten von Punkten werden relevante Konflikte erkannt und mithilfe der Technik der zylindrischen algebraischen Zerlegung verallgemeinert, was zu einer gröberen Zerlegung führt als die, die die ursprüngliche Methode berechnen würde. Obwohl die theoretische Komplexitätsgrenze nicht verbessert wird, lassen diese Methoden Raum für Heuristiken, die den Suchprozess leiten und die praktische Effizienz bei realen Problemen verbessern können. Diese Arbeit befasst sich mit einer Vielzahl von solchen explorationsgeleiteten Algorithmen. Wir identifizieren gemeinsame Teile dieser Algorithmen, um ihre Darstellung zu vereinheitlichen und Ideen zwischen diesen Methoden zu übertragen, um ihre praktische Effizienz weiter zu verbessern. Außerdem übertragen wir den explorationsgeleiteten Ansatz auf die Quantorenelimination, indem wir diese Algorithmen entsprechend erweitern. Bei der zylindrischen algebraischen Zerlegung wird der Raum implizit durch die Berechnung von Projektionspolynomen zerlegt. Die Menge der Projektionspolynome kann in explorationsgeleiteten Algorithmen reduziert werden, da wir nur eine auf einen bestimmten Konflikt zugeschnittene Zerlegung berechnen müssen. Da diese Projektionsmenge nach komplexeren Regeln bestimmt wird, formuliert diese Arbeit die Projektionsoperation als Beweissystem. Dies macht die Algorithmen erweiterbar für weitere Optimierungen, erhöht das Vertrauen in ihre Implementierung und definiert Schnittstellen für feinkörnige Heuristiken. Darüber hinaus ist es ein erster Schritt in Richtung von Zertifikaten, die die Korrektheit der Ausführung eines Solvers bezeugen. Auf der Grundlage des Beweissystems trägt diese Arbeit zu einer Reihe von Verbesserungen der Projektionsoperation bei und führt zu neuen Begriffen, die zum Verständnis der Theorie hinter der zylindrischen algebraischen Zerlegung beitragen. Darüber hinaus untersuchen wir einige Heuristiken, die die praktische Effizienz von explorationsgeleiteten Algorithmen verbessern. Die in dieser Arbeit vorgestellten Methoden werden anhand einer Implementierung im SMT-Solver SMT-RAT experimentell evaluiert.The first-order theory of the reals admits an expressive language with a variety of potential applications. The cylindrical algebraic decomposition method is a powerful tool from real algebra for answering different kinds of problems related to the theory of the reals, among them satisfiability of quantifier-free formulas, validity of sentences, and quantifier elimination. It decomposes the real space into finitely many subsets in which certain properties of the polynomials occurring in the input are invariant. The resulting decomposition is then used to conclude about properties of the input formula. Despite its doubly exponential complexity bound, up to today, the cylindrical algebraic decomposition method has been the foundation of most algorithms implemented in state-of-the-art tools. Satisfiability-modulo-theories solving is a technology for checking the satisfiability of quantifier-free first-order logic formulas over one or more theories. Modern solvers support a wide range of theories and are applied to real-world problems. In the past decade, these solvers have been extended to support also real arithmetic formulas, based on ideas from the cylindrical algebraic decomposition. Instead of computing a whole decomposition eagerly, these adaptations follow an exploration-guided approach: by guessing sample points, relevant conflicts are detected and generalized using technology from the cylindrical algebraic decomposition, yielding a coarser decomposition than what the original method would compute. Although the theoretical complexity bound is not improved, these methods allow room for heuristics that guide the search process and may improve practical efficiency on real-world problems. This thesis concerns a variety of such exploration-guided algorithms. We identify common parts of these algorithms to unify their presentation and transfer ideas between these methods, further improving their practical efficiency. Further, we transfer the exploration-guided approach to quantifier elimination by extending these algorithms accordingly. The cylindrical algebraic decomposition implicitly decomposes the space by computing projection polynomials. The set of projection polynomials can be reduced in exploration-guided algorithms, as we only need to compute a decomposition tailored towards a given conflict. As this projection set is determined according to more complex rules, this thesis formulates the projection operation as a proof system. This makes the algorithms extensible for further optimizations, increases the trust into their implementation, and defines interfaces for fine-grained heuristics. Further, it is a first step towards certificates witnessing the correctness of a solver's run. Based on the proof system, this thesis contributes a range of improvements to the projection operation, and leads to new notions that contribute to the understanding of the theory behind the cylindrical algebraic decomposition. We further examine some heuristics that improve the practical efficiency of exploration-guided algorithms. The methods presented in this thesis are experimentally evaluated based on an implementation in the SMT solver SMT-RAT.
OpenAccess: 
PDF
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online
Sprache
English
Externe Identnummern
HBZ: HT031325787
Interne Identnummern
RWTH-2025-09926
Datensatz-ID: 1022295
Beteiligte Länder
Germany
|
The record appears in these collections: |