On solving real-algebraic formulas in a satisfiability-modulo-theories framework

Loup, Ulrich; Ábrahám, Erika (Thesis advisor); Levandovskyy, Viktor (Thesis advisor); Sturm, Thomas (Thesis advisor)

Aachen (2018, 2019) [Dissertation / PhD Thesis]

Page(s): 1 Online-Ressource (ii, 222 Seiten) : Illustrationen, Diagramme

Abstract

Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations and inequalities over the domain of the real numbers. Coming with a strong expressiveness and a still decidable satisfiability problem, real-algebraic formulas are a precious modeling language in many academic, industrial and commercial areas. However, only some classes of real-algebraic formulas allow an efficient solving in practice. For instance, conjunctions of linear real-algebraic constraints can be solved with the very successful simplex method. The virtual substitution method can solve also formulas containing quadratic polynomials and, based on recent developments, also polynomials of higher degrees. Other examples are solving methods based on interval constraint propagation, which are able to deal with even more expressive formulas, e.g.~including trigonometric functions. Although those computations are not always terminating with a conclusive answer, they often lead to a reliable result in a short running time. Further special examples are solving techniques based on Gröbner bases. They can be used to solve real-algebraic formulas in combination with other techniques, making the implementation a challenging task. The general quantifier-free real-algebraic satisfiability problem, however, has a worst-case time complexity bound which is exponential in the number of input variables. Methods solving this general problem directly are often inefficient in practice. The most popular method in this respect is the cylindrical algebraic decomposition (CAD) method. Its search space can grow doubly-exponentially with the number of input variables. Thus, its practical usefulness highly depends on search heuristics and search space pruning. In this thesis, both aspects are shed light on. In particular, the CAD method is analyzed in combination with other more specialized solving methods such as Gröbner bases. Moreover, bounds to the variables are used to prune the CAD search space, especially when combining the method with interval-arithmetic techniques. This thesis tackles the solving of general quantifier-free real-algebraic formulas with a combination of different methods in a satisfiability-modulo-theories (SMT) framework: A SAT solver computes partial assignments for the Boolean structure of the real-algebraic formula and real-algebraic solvers check these assignments for consistency in the real domain. If the assignment is infeasible in the real domain, the SAT solver would profit from a small reason for this conflict in terms of a subset of the constraints corresponding to the conflicting assignment. Preferably minimal reasons are a valuable good in an SMT solver. As a main part, this thesis comprises a description and evaluation of their computation using the CAD method. In addition, the new and interesting approach for real-algebraic solving by computing realizable sign conditions is analyzed in terms of its adaptability to the SMT framework.

Identifier

  • REPORT NUMBER: RWTH-2018-231963

Downloads