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.

翻译：柱形代数分解（CAD）是实现实数量词消去（QE）的首个实用方法，至今仍是主流方法之一，自Collins原始方法提出以来已得到诸多改进。然而，其计算复杂度在变量数量上本质上具有双重指数级增长。在适用场景下，虚拟项代入（VTS）更为高效：单次应用可将含$n$个变量的QE问题转化为含$n-1$个变量的问题，并依此类推。因此，混合方法具有应用空间：在可行时采用VTS，随后使用CAD。本文基于第二作者的博士学位论文，描述了这种多算法融合的实现方案。所采用的CAD版本基于Lazard最近验证的方法的新实现，并针对等式约束处理进行了改进。