Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition

TL;DR

This work surveys recent advances in Real Quantifier Elimination and Cylindrical Algebraic Decomposition, emphasizing integration with SAT/SMT and the SC$^2$ ecosystem, as well as data-driven optimization of CAD. It highlights two main developments: (i) CAD-based algorithms that move beyond full decompositions toward search-guided coverings and theory solving within SMT, including NuCAD and MCSAT, and (ii) machine-learning-inspired tuning of CAD, notably variable ordering, supplemented by explainable AI techniques to extract actionable heuristics. The results suggest a practical pathway to push back the doubly exponential barrier by combining hybrid symbolic-logic methods with interpretable ML-guided heuristics. Collectively, these approaches broaden the applicability of QE/CAD to larger, more complex problems while maintaining reliability through explainability.

Abstract

This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.

Figures (5)

• Figure 1: Visualisation of sign-invariant CADs built for the polynomial $x^2+bx+1$. On the left: the polynomial is graphed as the dark solid curve with the seven 2D cells in the CAD the regions separated by the graph and the additional dotted lines. Note that the CAD also contains two point cells (the points where the tangent of the polynomial is vertical); and eight 1D cells (the curve segments of the polynomial's graph either side of the point cells and the vertical line segments at $x = \pm 2$ either side of the point cells). Each cell contains a sample point (solid circles). On the right: the sample points have been shaded green (lighter in greyscale) and red (darker in greyscale) depending on the truth of $x^2 + bx + 1 \leq 0$. The true cells have been projected onto the $b$-axis.
• Figure 2: These piles of grain demonstrate exponential growth (left) and doubly exponential growth (right). Image credit: Tereso del Río.
• Figure 3: Schematic of the Satisfiability Modulo Theory Paradigm
• Figure 4: Figure 15 from ADEK21. Demonstrating that a fewer number of polynomials (only those whose intersection with the shaded region is dotted) may be used to produce a covering than a decomposition (which would use all polynomials graphed).
• Figure 5: Two CADs for the same polynomial with full dimensional cells the connected regions between the graph and the additional horizontal lines. On the left the cells project into a single cylinder over the whole horizontal axis; while on the right they project onto multiple cylinders over the vertical axis.