h1

% IMPORTANT: The following is UTF-8 encoded.  This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.

@PHDTHESIS{Nalbach:1022295,
      author       = {Nalbach, Jasper Kurt Ferdinand},
      othercontributors = {Abraham, Erika and Davenport, James H.},
      title        = {{C}ylindrical algebraic decomposition based methods in
                      satisfiability modulo non-linear real arithmetic},
      school       = {RWTH Aachen University},
      type         = {Dissertation},
      address      = {Aachen},
      publisher    = {RWTH Aachen University},
      reportid     = {RWTH-2025-09926},
      pages        = {1 Online-Ressource : Illustrationen},
      year         = {2025},
      note         = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
                      University; Dissertation, RWTH Aachen University, 2025},
      abstract     = {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.},
      cin          = {123420},
      ddc          = {004},
      cid          = {$I:(DE-82)123420_20140620$},
      pnm          = {GRK 2236 - GRK 2236: Unsicherheit und Randomisierung in
                      Algorithmen, Verifikation und Logik. (282652900)},
      pid          = {G:(GEPRIS)282652900},
      typ          = {PUB:(DE-HGF)11},
      doi          = {10.18154/RWTH-2025-09926},
      url          = {https://publications.rwth-aachen.de/record/1022295},
}