Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Cylindrical Algebraic Decomposition in Macaulay2

Corin Lee, Tereso del Río, Hamid Rahkooy

TL;DR

This paper introduces CylindricalAlgebraicDecomposition, the first Macaulay2 implementation of CAD that yields an Open CAD for sets of rational-coefficient polynomials. It employs Lazard projection and a new gmods-based variable-ordering heuristic to reduce the number of full-dimensional cells, enabling efficient satisfiability checks for strict polynomial inequalities via findPositiveSolution. The RealRoots-based root isolation is integrated with targeted improvements to robustness and performance. The work enables practical open-CAD-based existential testing and outlines a path toward full CAD-based quantifier elimination and connectivity analysis, with potential impact in real algebraic geometry and related applications.

Abstract

CylindricalAlgebraicDecomposition.m2 is the first implementation of Cylindrical Algebraic Decomposition (CAD) in Macaulay2. CAD decomposes space into 'cells' where input polynomials are sign-invariant. This package computes an Open CAD (full-dimensional cells only) for sets of real polynomials with rational coefficients, enabling users to solve existential problems involving strict inequalities. With the construction of a full CAD (cells of all dimensions), this tool could be extended to solve any real quantifier elimination problem. The current implementation employs the Lazard projection and introduces a new heuristic for choosing the variable ordering.

Cylindrical Algebraic Decomposition in Macaulay2

TL;DR

This paper introduces CylindricalAlgebraicDecomposition, the first Macaulay2 implementation of CAD that yields an Open CAD for sets of rational-coefficient polynomials. It employs Lazard projection and a new gmods-based variable-ordering heuristic to reduce the number of full-dimensional cells, enabling efficient satisfiability checks for strict polynomial inequalities via findPositiveSolution. The RealRoots-based root isolation is integrated with targeted improvements to robustness and performance. The work enables practical open-CAD-based existential testing and outlines a path toward full CAD-based quantifier elimination and connectivity analysis, with potential impact in real algebraic geometry and related applications.

Abstract

CylindricalAlgebraicDecomposition.m2 is the first implementation of Cylindrical Algebraic Decomposition (CAD) in Macaulay2. CAD decomposes space into 'cells' where input polynomials are sign-invariant. This package computes an Open CAD (full-dimensional cells only) for sets of real polynomials with rational coefficients, enabling users to solve existential problems involving strict inequalities. With the construction of a full CAD (cells of all dimensions), this tool could be extended to solve any real quantifier elimination problem. The current implementation employs the Lazard projection and introduces a new heuristic for choosing the variable ordering.

Paper Structure

This paper contains 27 sections, 1 theorem, 7 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Cylindrical Algebraic Decomposition
  4. Brief history
  5. CAD basics
  6. CAD construction
  7. Choices made for the package
  8. Variable ordering
  9. Lazard projection
  10. Open CAD
  11. RealRoots improvements
  12. The CylindricalAlgebraicDecomposition package
  13. Package Overview
  14. openCAD
  15. positivePoint
  16. ...and 12 more sections

Key Result

Theorem 2.1

Let $\mathcal{F}$ be a non-empty set of non-zero real polynomials in $n\geq 2$ real variables. Let $S$ be a connected subset of $\mathbb{R}^{n-1}$. If every element of the projection of $\mathcal{F}$ is sign-invariant on $S$, then the polynomials in $\mathcal{F}$ are delineable over $S$.

Figures (7)

  • Figure 1: Algebraic varieties of $3-x^2$ (blue) and $(7x-12)(x^2+x+1)$ (orange), and the associated values of $x$ ensuring these polynomials are positive (blue and orange highlighting, respectively).
  • Figure 2: The graph of $\mathcal{F}=\{x^2+y^2-1\}$ and its associated sign-invariant CAD of $\mathbb{R}^2$. This CAD consists of 13 cells: five 2-cells (the coloured regions), six 1-cells (the lines between them) and two 0-cells (the two red points where the lines meet). The black crosses represent the sample points for each cell. These cells stack in cylinders over the five cells of the CAD of $\mathbb{R}^1$ (the two points at the bottom and the regions between them). Each cell is described by constraints on $x$ and $y$.
  • Figure 3: Illustration of delineability, from Brown2004.
  • Figure 4: CADs sign-invariant for the set of polynomials $\{x^5+5 x^4+5 x^3-5 x^2-6x-2y\}.$ Using ordering $y \prec x$, we obtain a CAD with 57 cells (18 2-cells, 27 1-cells and 12 0-cells). Using the ordering $x \prec y$ generates only three cells (two 2-cells and one 1-cell).
  • Figure 5: List of functions contained in the CylindricalAlgebraicDecomposition package. Methods labelled in blue are from external packages.
  • ...and 2 more figures

Theorems & Definitions (4)

  • Definition 1: Cylindrical Algebraic Decomposition
  • Theorem 2.1: Collins75, Theorem 5
  • Definition 2
  • Definition 3: Lazard projection