2011/12/22 by Hari Krishna Malladi, Malladi, Hari Krishna, Ambedkar Dukkipati +1
Computer Science · #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #VLSI and Analog Circuit Testing #cs.DM
paper · pdf · doi:10.48550/arxiv.1112.5352
8 pages
openalex publication_date 2011/12/22 · arxiv created 2013/01/21 · arxiv updated 2013/01/22 · openalex created_date 2022/09/01 · openalex updated_date 2026/07/28
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.