parallelize CAD [@issac89]. In spite of all these improvements, the fact that CAD’s time complexity is doubly exponential makes quantifier elimination through CAD impossible for a wide range of real-world applications.

Parallelism has appeared to be the trend, while addressing algorithms which have a significant amount of independence in their structure. Speeding up executions by scaling the existing CPU speeds has been found to be inefficient. The maximum possible clock speed has remained at around 3 GHz for the past 12 years, for a desktop microprocessor, in spite of being scaled by about 100 times in the 1990s. Multicores have achieved prominence, as dual-cores and quad-cores have become ubiquitous in the past 7 years. This suggests that the only major way to improve an existing algorithm’s running time is through parallelism. We use this as a motivation to introduce an input-level parallelism in the CAD algorithm.

In this paper, we study a possibility to preprocess the input prenex formula, so that several instances of CAD can be run in parallel on it. Input-level parallelism is not directly applicable to CAD because of the constraints imposed by first-order logic itself. Thus, clause normal forms and virtual substitutions are used to ‘separate’ 