Exploiting strict constraints in the computation of cylindrical algebraic coverings

• Ausnutzung von strikten Ungleichungen zur Berechnung von zylindrischen, algebraischen Abdeckungen

Bär, Philipp; Ábrahám, Erika (Thesis advisor); Giesl, Jürgen (Thesis advisor); Nalbach, Jasper Kurt Ferdinand (Consultant)

Aachen : RWTH Aachen University (2023)
Bachelor Thesis

Bachelorarbeit, RWTH Aachen University, 2022

Abstract

Satisfiability Modulo Theories (SMT) solving is a technique used to determine the satisfiability of Quantifier-free First-order Logic formulae over a fixed theory. The Cylindrical Algebraic Decomposition (CAD) method is a commonly used strategy for solving problems of Non-linear Real Arithmetic. Recently, the Cylindrical Algebraic Covering (CAlC) method has been developed, which is a variant of the CAD method that incrementally tries to construct a satisfying solution for a conjunction of polynomial constraints or to detect its unsatisfiability. On the basis of a given variable and a partial assignment to some other variables, the main principle of the CAlC method is to generate single real values and open intervals of real numbers which can be omitted when searching for a satisfying solution.We present two adaptions of the CAlC method that exploit strict constraints in the input conjunction. Both aim at extending the generated open intervals to include some of their endpoints in order to speed up the computation.

Institutions

• Department of Computer Science [120000]
• Theory of Hybrid Systems Research Group [123420]