Projection and Quantifier Elimination Using Non-uniform Cylindrical Algebraic Decomposition

Cylindrical Algebraic Decomposition (CAD) is an established tool in the computer algebra community for computing with semi-algebraic sets / Tarski formulas. The key property of CAD is that it provides a representation in which geometric projection and set complement (the analogues of the logical operations of quantifier elimination and negation for Tarski formulas) are trivial. However, constructing a CAD often requires an impractical amount of time and space. Non-uniform CAD (NuCAD) was introduced with the goal of providing a more practically efficient alternative to CAD for computing with semi-algebraic sets / Tarski formulas. As a first step towards that goal, previous work has shown that Open NuCADs do provide a much more efficient representation than Open CADs. However, it hasn't been shown that the key operation of projection can be computed efficiently in the NuCAD representation, because while set complement is trivial for NuCADs, as it is for CADs, projection, in contrast to the CAD case, is not. This paper provides another step towards the larger goal by showing how projection can be done efficiently in the Open NuCAD representation. The importance of this contribution is not restricted to Open NuCADs, since the same approach to projection will carry over to the general case for NuCADs where, we hope, the practical benefits of the much smaller representation NuCAD provides will be even greater.