量词消除的多算法方法
摘要：圆柱代数分解（CAD）是第一个实际进行实数量词消除（QE）的有效方法，至今仍然是一种重要的方法，并且自Collins最初的方法以来有许多改进。然而，它的复杂性在本质上是随着变量数量的双指数增长。在适用的情况下，虚拟术语替换（VTS）更有效，可以将$n$个变量的QE问题转化为一个应用中的$n-1$个变量问题，依此类推。因此，存在混合方法的空间：在可能的情况下使用VTS，然后再使用CAD。 本文描述了这种基于第二作者的博士论文的多算法实现。所使用的CAD版本基于Lazard最近证明的方法的新实现，并进行了一些改进以处理方程约束。
作者：James H. Davenport and Zak P. Tonks and Ali K. Uncu
论文ID：2302.06814
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2023-02-15