a given input formula so that it’s components can be executed in parallel using existing CAD implementations. We study the preprocessor algorithm through extensive experimentation using the QEPCAD B tool, running several instances on a cluster.

The work by Saunders et. al. [@issac89] has brought up the notion of a parallel version of CAD, where they introduce an execution-level parallelism to make the phases of CAD work in parallel. Since our work introduced input-level parallelism, our preprocessor can be used along with Saunders’ approach.

The paper is organized as follows. The preliminary notations and the original CAD algorithm are briefly introduced in Section 2. The use of clause normal forms and virtual substitutions and the preprocessor itself are described in Section 3. In Section 4, we introduce some notions to define structure in a prenex formula. An experimental characterization of the preprocessor algorithm, are presented in Section 5. Extensions sought for the proposed algorithm and a few concluding remarks have been made in Section 6.

Preliminaries
=============

Basic Definitions and Notation
------------------------------

Let $k [x_1,. . .,x_n]$ denote the set of all polynomials in variables, $ x_1,. . .,x_n $ and coefficients from the field $k $. The base field, 