2025/08/01 by Jasper Nalbach, Nalbach, Jasper, Erika Ábrahám +1
Computer Science · #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Formal Methods in Verification #Polynomial and algebraic computation #Symbolic Computation (cs.SC)
paper · pdf · doi:10.48550/arxiv.2508.00505
openalex publication_date 2025/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.