Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition

TL;DR

This paper surveys recent advances in real quantifier elimination and cylindrical algebraic decomposition, highlighting algorithmic adaptations inspired by SAT/SMT and the integration of machine learning for optimization.

Contribution

It introduces recent developments in CAD and QE, including adaptations from computational logic, SMT integration, and ML-based optimization techniques.

Findings

CAD algorithms inspired by SAT/SMT improve efficiency.

Machine learning enhances CAD variable ordering.

Explainable AI offers insights without ML reliance.

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.