A Poly-algorithmic Approach to Quantifier Elimination

TL;DR

This paper introduces a hybrid poly-algorithm combining virtual term substitution and cylindrical algebraic decomposition for more efficient real quantifier elimination, leveraging recent improvements in CAD implementation.

Contribution

It presents a novel hybrid approach that integrates VTS and CAD, including a new CAD implementation with enhancements for equational constraints.

Findings

Hybrid method improves efficiency of quantifier elimination.

New CAD implementation handles equational constraints effectively.

Combines strengths of VTS and CAD for practical QE solutions.

Abstract

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.