This article explores the algorithmic tool called Cylindrical Algebraic Decomposition (CAD) and its application in Real Quantifier Elimination (QE). These topics are important in symbolic computation and have recently gained renewed interest in the development of SMT solvers for non-linear real arithmetic. The article begins by discussing the limitations of iterated univariate resultants in traditional CAD, especially when dealing with multiple equational constraints. It proposes the use of multivariate resultants in the projection phase of CAD as a more efficient alternative. The article also delves into an alternative approach to this problem documented in a previous paper, which redefines the object under construction but only applies to two equational constraints. Important clarifications, corrections, and proofs are provided in relation to this approach. Lastly, the article addresses SMT or Real QE problems expressed using rational functions and their prevalence in industrial applications. It revisits a proposal for handling satisfiability in these cases and offers an alternative approach for more complicated quantification structures.
Abstract:This paper builds and extends on the authors previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic.
First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport & England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum & Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an important typo and provide a missing proof in that paper.
We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative.