---
abstract: 'The Cylindrical Algebraic Decomposition (CAD) algorithm is a comprehensive tool to perform quantifier elimination over real closed fields. CAD has doubly exponential running time, making it infeasible for practical purposes. We propose to use the notions of clause normal forms and virtual substitutions to develop a preprocessor for CAD, that will enable an input-level parallelism. We study the performance of CAD in the presence of the preprocessor by extensive experimentation. Since parallelizability of CAD depends on the structure of given prenex formula, we introduce some structural notions to study the performance of CAD with the proposed preprocessor.'
author:
- |
    Hari Krishna Malladi    and    Ambedkar Dukkipati\
    \
bibliography:
- 'harikrishnamalladi.bib'
date:
- 31 December 2011
- 8 June 2012
title: |
    **A Preprocessor Based on Clause Normal Forms and Virtual Substitutions to Parallelize\
    Cylindrical Algebraic Decomposition**
---

Introduction
============

The study of real algebraic geometry deals with the study of the real roots of an equation as, more often than not, the real roots are the most desired solutions to a system of equations. It is important to note that for some problems there are no counterparts in complex algebraic geometry. Given a first-order formula in real algebraic 