Iterated Resultants and Rational Functions in Real Quantifier Elimination
CoRR(2023)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要