Simple CAD Construction and its Applications

This paper presents a method for the simplification of truth-invariant cylindrical algebraic decompositions (CADs). Examples are given that demonstrate the usefulness of the method in speeding up the solution formula construction phase of the CAD-based quantifier elimination algorithm. Applications of the method to the construction of truth-invariant CADs for very large quantifier-free formulas and quantifier elimination of non-prenex formulas are also discussed.