h1

001022295 001__ 1022295
001022295 005__ 20251211084601.0
001022295 0247_ $$2HBZ$$aHT031325787
001022295 0247_ $$2Laufende Nummer$$a44813
001022295 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-09926
001022295 037__ $$aRWTH-2025-09926
001022295 041__ $$aEnglish
001022295 082__ $$a004
001022295 1001_ $$0P:(DE-82)IDM04423$$aNalbach, Jasper Kurt Ferdinand$$b0$$urwth
001022295 245__ $$aCylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic$$cvorgelegt von Jasper Nalbach, Master of Science$$honline
001022295 260__ $$aAachen$$bRWTH Aachen University$$c2025
001022295 300__ $$a1 Online-Ressource : Illustrationen
001022295 3367_ $$02$$2EndNote$$aThesis
001022295 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
001022295 3367_ $$2BibTeX$$aPHDTHESIS
001022295 3367_ $$2DRIVER$$adoctoralThesis
001022295 3367_ $$2DataCite$$aOutput Types/Dissertation
001022295 3367_ $$2ORCID$$aDISSERTATION
001022295 502__ $$aDissertation, RWTH Aachen University, 2025$$bDissertation$$cRWTH Aachen University$$d2025$$gFak09$$o2025-11-12
001022295 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
001022295 5203_ $$aDie 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.$$lger
001022295 520__ $$aThe 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.$$leng
001022295 536__ $$0G:(GEPRIS)282652900$$aGRK 2236 - GRK 2236: Unsicherheit und Randomisierung in Algorithmen, Verifikation und Logik. (282652900)$$c282652900$$x0
001022295 588__ $$aDataset connected to Lobid/HBZ
001022295 591__ $$aGermany
001022295 653_7 $$acylindrical algebraic decomposition
001022295 653_7 $$anon-linear real arithmetic
001022295 653_7 $$aquantifier elimination
001022295 653_7 $$areal algebra
001022295 653_7 $$asatisfiability modulo theories
001022295 7001_ $$0P:(DE-82)IDM00047$$aAbraham, Erika$$b1$$eThesis advisor$$urwth
001022295 7001_ $$aDavenport, James H.$$b2$$eThesis advisor
001022295 8564_ $$uhttps://publications.rwth-aachen.de/record/1022295/files/1022295.pdf$$yOpenAccess
001022295 8564_ $$uhttps://publications.rwth-aachen.de/record/1022295/files/1022295_source.zip$$yRestricted
001022295 909CO $$ooai:publications.rwth-aachen.de:1022295$$pdnbdelivery$$pdriver$$pVDB$$popen_access$$popenaire
001022295 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
001022295 9141_ $$y2025
001022295 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM04423$$aRWTH Aachen$$b0$$kRWTH
001022295 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00047$$aRWTH Aachen$$b1$$kRWTH
001022295 9201_ $$0I:(DE-82)123420_20140620$$k123420$$lLehr- und Forschungsgebiet Theorie Hybrider Systeme$$x0
001022295 961__ $$c2025-12-10T14:08:27.465994$$x2025-11-24T11:09:12.076117$$z2025-12-10T14:08:27.465994
001022295 9801_ $$aFullTexts
001022295 980__ $$aI:(DE-82)123420_20140620
001022295 980__ $$aUNRESTRICTED
001022295 980__ $$aVDB
001022295 980__ $$aphd