Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
Matthew England

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
