This paper introduces an improved method for constructing cylindrical algebraic decompositions (CADs) for formulas with two polynomial equations as implied constraints. The fundamental idea is that neither of the varieties of these two polynomials is actually represented by the CAD produced by this method, only the variety defined by their common zeros is represented by the CAD. This allows for a substantially smaller projection factor set, and thus for a CAD with many fewer cells. The special case of formulas containing two polynomial equations as constraints is an important one, but this work is also intended to be extended in the future to the case of many constraint equations.

In the current theory of CADs, the fundamental object is to decompose n-dimensional space into regions in which a polynomial equation f = 0 is either identically true or identically false. With many polynomials, we seek a decomposition into regions in which each polynomial equation is identically true or false independently. The results presented here are intended to be the first step in establishing a theory of CADs in which systems of equations are fundamental objects, so that given a system we seek a decomposition into regions in which the system of equations is identically true or false --- which means each equation is no longer considered independently. Quantifier elimination problems of this form (systems of equations with inequalities as side conditions) are quite common, and this approach has the potential to bring large problems of this type into the scope of what can be solved in practice.