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新近验证方法的新实现，并针对等式约束进行了若干改进。