and Cardano’s formulas for quartics and cubics involve complex roots, and hence cannot be used. For quintic and higher order polynomials, there exists no generic closed form solution, as proved by Abel.

We would like to use the algorithm to perform virtual substitutions by Volker Weispfenning [@weispfenning]. While Weispfenning’s work on virtual substitution seeks to find a quantifier-free equivalent by itself, we would like to adapt it to minimize dependencies within the clauses and hence, to increase parallelism.

In our notion of substitutability, we classify polynomials into two classes, namely (i) substitutor and (ii) substituend.

A ‘substitutor’ polynomial is used to substitute for a variable in other polynomials. A ‘substituend’ polynomial is one, in which a variable is replaced.Assume that $P$ is any polynomial and $T$ is a substitutor. We say that $T$ is ‘substitutable’ in $P$ if, the process of replacing a variable in $P$ by virtual substitution results in a decrease in the number of variables in the polynomial $P$.

We use the results proved by Weispfenning and Christopher Brown [@brownsub], which state that virtual substitution leads to an equi-satisfiale formula.

The Proposed Preprocessor
-------------------------

In this section we present a preprocessor to the CAD algorithm that is 