Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing real quantifier elimination (QE), and is still a major method, with many improvements since Collins' original method. Nevertheless, its complexity is inherently doubly exponential in the number of variables. Where applicable, virtual term substitution (VTS) is more effective, turning a QE problem in $n$ variables to one in $n-1$ variables in one application, and so on. Hence there is scope for hybrid methods: doing VTS where possible then using CAD. This paper describes such a poly-algorithmic implementation, based on the second author's Ph.D. thesis. The version of CAD used is based on a new implementation of Lazard's recently-justified method, with some improvements to handle equational constraints.
翻译:Cylindrical Algebraic Decomposition(CAD)是真正消除量化因素(QE)的第一个实际手段,仍然是一个重要的方法,自Collins最初采用的方法以来有许多改进。然而,其复杂性在变量数量上具有内在的双重指数性。在适用的情况下,虚拟术语替代(VTS)更为有效,将一个零美元变量的量化替代问题变成一个零美元变量的1美元变量,等等。因此,存在混合方法的可能性:在可能情况下,采用VTS,然后使用CAD。本文根据第二作者的Ph.D论文描述了这种多数值的落实。使用的CAD版本基于新实施Lazard最近调整的方法,并用一些改进来处理方程式限制。