A Preprocessor Based on Clause Normal Forms and Virtual Substitutions to Parallelize Cylindrical Algebraic Decomposition

TL;DR

This paper introduces a preprocessor leveraging clause normal forms and virtual substitutions to enable input-level parallelism in Cylindrical Algebraic Decomposition, aiming to mitigate its doubly exponential complexity.

Contribution

It presents a novel preprocessor for CAD based on clause normal forms and virtual substitutions, facilitating parallel computation and improving performance.

Findings

Preprocessor enables input-level parallelism in CAD.

Experimental results show performance improvements.

Structural notions help predict CAD's parallelizability.

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.