guest ::
TY - THES AU - Nalbach, Jasper Kurt Ferdinand TI - Cylindrical algebraic decomposition based methods in satisfiability modulo non-linear real arithmetic PB - RWTH Aachen University VL - Dissertation CY - Aachen M1 - RWTH-2025-09926 SP - 1 Online-Ressource : Illustrationen PY - 2025 N1 - Veröffentlicht auf dem Publikationsserver der RWTH Aachen University N1 - Dissertation, RWTH Aachen University, 2025 AB - 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. LB - PUB:(DE-HGF)11 DO - DOI:10.18154/RWTH-2025-09926 UR - https://publications.rwth-aachen.de/record/1022295 ER -