Skip to content

Cylindrical Algebraic Decomposition

Partition real coordinate space into finitely many connected semialgebraic cells that are cylindrically compatible under projection and sign-invariant for a declared polynomial family.

Version
v3 · 2026-09-19 · History
Domain-specific #
1614
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomain
Real Algebraic Geometry → Mathematics
Aliases
CAD, Cylindrical decomposition

Core Idea

Given a finite polynomial set \(P\subset \mathbb{R}[x_1,\ldots,x_n]\) and an ordering of the variables, a cylindrical algebraic decomposition (CAD) partitions \(\mathbb{R}^n\) into finitely many connected semialgebraic cells. Every polynomial in \(P\) has constant sign on each cell, and the cells are cylindrical: projections of two cells onto any lower-dimensional initial coordinate space are either identical or disjoint.[1]

CAD is both the resulting decomposition and a family of algorithms for constructing it. The classical projection-and-lifting method recursively derives lower-dimensional projection polynomials, decomposes the real line, and lifts stacks of sections and sectors over lower-dimensional cells.[2] Sign- or truth-invariance then turns quantified polynomial formulas into finite cellwise decisions.

How would you explain it like I'm…

Cutting Paper Into Same-Side Pieces

Draw some curvy lines on a sheet of paper. Now cut the paper into pieces so that each piece is completely on one side of every line, or sits right on a line. You also cut in neat up-and-down columns, so pieces stack on top of each other. Then to answer a question about the whole paper, you just check one spot in each piece.

Stacked Sign-Keeping Pieces

A cylindrical algebraic decomposition cuts space into a finite number of pieces, called cells, based on some polynomial equations. In each cell, every polynomial stays the same sign: always positive, always negative, or always zero. The cutting is done in an orderly, column-by-column way: you split one direction first, then build stacks of cells above each piece. Because the answer doesn't change inside a cell, you can check a question about the whole space just by testing one point in each cell. It is also the name of the computer method for building these pieces.

Sign-Invariant Cylindrical Cells

A cylindrical algebraic decomposition (CAD) takes a finite list of polynomials in variables x₁, …, xₙ, with a chosen order for the variables, and splits all of n-dimensional real space into finitely many connected pieces called cells. On every cell, each polynomial has a constant sign: always positive, always negative, or always zero. The decomposition is cylindrical, meaning the cells line up in columns: if you project two cells down onto the first few coordinates, their shadows are either exactly the same or don't overlap. CAD also names the algorithms that build such decompositions, usually by projecting down one dimension at a time and then lifting back up, stacking cells over lower-dimensional ones. Because each cell is sign-uniform, questions involving "for all" and "there exists" about polynomial inequalities can be decided by checking finitely many cells.

 

Given a finite set P ⊂ ℝ[x1, …, xn] and a fixed variable ordering, a cylindrical algebraic decomposition is a partition of ℝ^n into finitely many connected semialgebraic cells such that every polynomial in P is sign-invariant on each cell. Cylindricity means that for each k < n, the projections of any two cells onto ℝ^k (the initial k coordinates) are either identical or disjoint, so the cells over each lower-dimensional cell form a stack. CAD names both the decomposition and algorithms for computing it. The classical projection-and-lifting method recursively computes projection polynomials in fewer variables until reaching one variable, decomposes ℝ into roots and open intervals, and then lifts: over each lower-dimensional cell it builds a stack of sections (graphs of root functions) and sectors (regions between them). Since each cell has constant signs, or more generally constant truth values of the relevant formulas, a quantified polynomial formula can be decided by evaluating it at sample points, one per cell. This makes CAD a central tool for real quantifier elimination.

Structural Signature

  • A real closed coefficient field, usually represented through real algebraic numbers.
  • A finite input family of multivariate polynomials.
  • A fixed variable ordering.
  • A finite partition of \(\mathbb{R}^n\) into connected semialgebraic cells.
  • Sign invariance, or an explicitly declared weaker truth/order invariance, on every cell.
  • Cylindrical compatibility of cell projections.
  • Projection operators producing lower-dimensional critical polynomials.
  • Recursive base decomposition and lifting into cell stacks.
  • Sample points representing cells for finite evaluation.
  • Exact algebraic-number isolation and sign determination.
  • Quantifier elimination or semialgebraic analysis as the readout.
  • A worst-case complexity that can be doubly exponential in the number of variables.

What It Is Not

CAD is not an arbitrary decomposition into geometric pieces: cells must satisfy a polynomial invariance condition and coordinate-projection cylindricity. It is not triangulation, mesh generation, or cubical subdivision. It is not Gröbner-basis elimination, which works through polynomial ideals over algebraic closures. It is not Fourier–Motzkin elimination, whose carrier is a finite system of linear inequalities. Nor is every use of sampled points a CAD; the surrounding cells and invariants are essential.

Scope of Application

CAD supports quantifier elimination over real closed fields, satisfiability of polynomial equalities and inequalities, real root classification, theorem proving, control and stability analysis, robot motion planning, and geometric constraint solving. It is especially valuable when the answer must be exact and described by semialgebraic conditions.[3]

The method is limited by cell growth, coefficient growth, algebraic-number costs, and sensitivity to variable ordering and projection choice. Partial, equational-constraint-aware, truth-table-invariant, and problem-specific variants reduce work without erasing the defining cylindrical-cell architecture.

Clarity

State the coefficient domain, input formula or polynomial set, variable ordering, projection operator, invariance target, treatment of nullification, cell representation, and whether the output is a full, partial, sign-invariant, or truth-invariant CAD. Distinguish the decomposition from the algorithm and distinguish logical quantifier order from the implementation's coordinate order.

Manages Complexity

CAD replaces a continuum of real assignments with finitely many cells on which all relevant sign or truth values are stable. One sample point can therefore represent every point in a cell for the declared decision task. Projection records where behavior can change; lifting reconstructs only the stratified cases that those critical values require. This is a decisive representational compression even when the number of cells is itself large.

Abstract Reasoning

  1. Normalize the polynomial formula and select a variable ordering.
  2. Choose a sound projection operator for the desired invariant.
  3. Project critical coefficients, discriminants, and resultants into fewer variables.
  4. Isolate the roots at the one-dimensional base.
  5. Form point sections and open sectors.
  6. Lift each lower-dimensional cell by specializing the next-variable polynomials at its sample point.
  7. Verify delineability and handle nullification according to the algorithm.
  8. Repeat until cells cover the full space.
  9. Evaluate signs or formula truth at cell samples.
  10. Propagate cellwise results through the quantifier structure.

Knowledge Transfer

The portable pattern is project the possible boundaries of behavioral change, partition a simpler space, then lift invariant regions back dimension by dimension. It transfers to stratified decision procedures and exact configuration-space reasoning. The proposed immediate parent is Decomposition.

Examples

For \(P=\{y-x^2\}\) with ordering \(x\prec y\), the parabola is a section; the regions above and below it are sectors on which the polynomial is respectively positive and negative. A compatible CAD further partitions the base where projected critical values require it. Evaluating one sample from each cell decides formulas such as \(\exists y\,(y=x^2\land y<1)\) after respecting the specified free and quantified variables.

For several polynomials, resultants expose parameter values at which roots meet, while discriminants expose multiple roots. These projection boundaries are sufficient only under the hypotheses of the selected projection theorem.

Structural Tensions

  • Exact logical completeness versus combinatorial explosion.
  • Full sign invariance versus task-specific truth invariance.
  • Fewer projection polynomials versus stronger well-orientedness obligations.
  • Favorable variable ordering versus quantifier-order constraints.
  • Symbolic exactness versus costly algebraic-number arithmetic.
  • Global decomposition versus partial exploration of relevant cells.

Structural–Framed Character

Recursive partition, boundary projection, lifting, and representative evaluation are structural. Real polynomial signs, semialgebraic connected cells, coordinate cylindricity, resultants, discriminants, and real-closed-field semantics are constitutive. The identity is domain-specific rather than a prime abstraction.

Structural Core vs. Domain Accent

The portable core is project change boundaries -> partition lower dimension -> lift invariant regions -> decide by representatives. The domain accent is exact real algebraic geometry with polynomial sign or formula-truth invariance.

This entry is a kind of Decomposition.

Decomposition is the broader abstraction this entry instantiates. Projection, Recursion, Invariance, Partition, Constraint, and Decision are related abstractions. Quantifier Elimination is a major application and related identity, not a synonym for CAD.

Relationships to Other Abstractions

Local relationship map for Cylindrical Algebraic DecompositionParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Cylindrical AlgebraicDecompositionDOMAINPrime abstraction: Decomposition — is a kind ofDecompositionPRIME

Current abstraction Cylindrical Algebraic Decomposition Domain-specific

Parents (1) — outgoing typed relations

  • Cylindrical Algebraic Decomposition is a kind of Decomposition Prime

    Decomposition is the broader abstraction this entry instantiates.

Hierarchy path (1) — routes to 1 parentless root

  • Cylindrical Algebraic Decomposition → is a kind of Decomposition

Neighborhood in Abstraction Space

Cylindrical Algebraic Decomposition sits in a sparse region of the domain-specific corpus (88th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Field Extensions & Galois-Theoretic Structures (19 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-25

Not to Be Confused With

  • Arbitrary cell decomposition.
  • Triangulation or finite subdivision.
  • Gröbner-basis elimination.
  • Fourier–Motzkin elimination.
  • Numerical meshing or sampling.
  • Tarski's original quantifier-elimination procedure.
  • A decomposition invariant only at tested points.

References

[1] George E. Collins, “Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition,” in Automata Theory and Formal Languages, LNCS 33 (Springer, 1975): 134–183, doi:10.1007/3-540-07407-4_17. registry ↩

[2] George E. Collins and Scott McCallum, “Cylindrical Algebraic Decomposition I: The Basic Algorithm,” Purdue University Computer Science Technical Reports 351 (1982), https://docs.lib.purdue.edu/cstech/351/. registry ↩

[3] Saugata Basu, Richard Pollack, and Marie-Françoise Roy, Algorithms in Real Algebraic Geometry, 2nd ed. (Springer, 2006), doi:10.1007/3-540-33099-2. registry ↩

[4] James H. Davenport and Joos Heintz, “Real Quantifier Elimination is Doubly Exponential,” Journal of Symbolic Computation 5 (1988): 29–35, doi:10.1016/S0747-7171(88)80004-X. registry ↩