Affordable Access

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

Authors
Type
Preprint
Publication Date
Submission Date
Identifiers
arXiv ID: 1112.5352
Source
arXiv
License
Yellow
External links

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.

Statistics

Seen <100 times