Given a set S of polynomials in Rn, a cylindrical algebraic decomposition is a decomposition of Rn into connected semialgebraic sets called cells, on which each polynomial has constant sign, either +, − or 0.
This implies that the images by π of the cells define a cylindrical decomposition of Rn−k.
Collins' algorithm has a computational complexity that is double exponential in n. This is an upper bound, which is reached on most entries.
There are also examples for which the minimal number of cells is doubly exponential, showing that every general algorithm for cylindrical algebraic decomposition has a double exponential complexity.
CAD provides an effective version of quantifier elimination over the reals that has a much better computational complexity than that resulting from the original proof of Tarski–Seidenberg theorem.