New Directions in Cylindrical Algebraic Decomposition

Matthew England, Coventry University, UK

Workshop on Real Algebraic Geometry and Algorithms for Geometric Constraint Systems

Date and Time: Tuesday, June 15, 2021 - 12:40pm to 1:20pm

Abstract: Cylindrical Algebraic Decomposition (CAD) is a key algorithm and data structure for answering questions about non-linear polynomial constraints, such as quantifier elimination. However, it suffers from doubly exponential complexity in the number of variables limiting its applicability in practice. We will survey two recent new directions of research.

First, the development of algorithms that utilise CAD theory in a search-based framework for answering questions like the satisfiability of formulae made of such constraints, or the consistency of sets of such constraints. These algorithms are inspired by, and sometimes used in combination with, those from the SAT/SMT community.

Secondly, work on the heuristics that take decisions when computing a CAD, such as the variable ordering. These decisions do not affect the mathematical correctness of the output but can have a great impact on the presentation of that output and the resources required to generate it. Recent experiments show that machine learning algorithms can offer better performance than human-designed heuristics.