Cylindrical Algebraic Decomposition

Draw the curve $x^2 + y^2 - 4 = 0$ on a sheet of paper. It slices the plane into two pieces: inside the circle the polynomial is negative, outside it is positive. On the curve itself it is exactly zero. Three simple regions, one clean rule for each.

Now imagine you are handed five or six polynomials in several variables at once, all tangled together. The curves and surfaces they define can carve space into hundreds of pieces. Cylindrical Algebraic Decomposition (CAD) is the recipe for finding that map automatically: it splits space into a finite list of cells, and inside each cell every one of your polynomials keeps a constant sign — always positive, always negative, or always zero, with no surprises hiding inside a cell.

Once you have that map, an enormous class of questions about real numbers stops being "search forever" and becomes "look up which cells satisfy the answer." That is the whole idea behind CAD, and it is the engine that makes quantifier elimination over the real numbers possible at all.

Below is a small plane with two fixed polynomials, $f(x,y) = x^2 + y^2 - 4$ (a circle) and $g(x,y) = y - x^2$ (a parabola). Press Decompose and watch the grid get shaded by the sign pattern of $(f, g)$ at each point: four colors for the four sign combinations, plus thin curves where a polynomial is exactly zero.

<p class="hint">{{hint_para}}</p>
<div class="stage">
  <canvas id="board" width="360" height="360"></canvas>
  <div class="legend">
    <div class="row"><span class="swatch pp"></span>{{legend_pp}}</div>
    <div class="row"><span class="swatch pm"></span>{{legend_pm}}</div>
    <div class="row"><span class="swatch mp"></span>{{legend_mp}}</div>
    <div class="row"><span class="swatch mm"></span>{{legend_mm}}</div>
    <div class="row"><span class="swatch curve"></span>{{legend_curve}}</div>
  </div>
</div>
<div class="status" id="status">{{status_initial}}</div>
<div class="btns">
  <button id="decompose" type="button">{{btn_decompose}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.stage { display: flex; gap: 1rem; flex-wrap: wrap; align-items: flex-start; }
canvas { border-radius: 8px; border: 1px solid #cdd9e3; cursor: crosshair; background: #fff; }
.legend { display: flex; flex-direction: column; gap: .35rem; font-size: .82rem; min-width: 170px; }
.row { display: flex; align-items: center; gap: .5rem; }
.swatch { width: 16px; height: 16px; border-radius: 4px; display: inline-block; border: 1px solid rgba(0,0,0,.15); }
.swatch.pp { background: #cdeccd; }
.swatch.pm { background: #f6d6a6; }
.swatch.mp { background: #a9d3f2; }
.swatch.mm { background: #e3b8d6; }
.swatch.curve { background: #1d3557; }
.status { font-size: 1rem; font-weight: 600; margin: .6rem 0; min-height: 1.4em; color: #1d3557; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Click any cell to see its sign pattern printed out. Notice that every point inside one shaded region gives the exact same pattern — that constancy is the entire point of CAD. A real algorithm would find the curves first (algebraically, not by scanning pixels) and then describe each resulting cell exactly; our demo scans a grid to make the same regions visible.

Why does anyone care about a fancy way to color a plane? Because the same construction works in any number of variables, and it settles a question that looks hopeless at first glance.

• The problem it solves: take any formula built from polynomial equations and inequalities, combined with $\exists$ (there exists) and $\forall$ (for all) over real variables — for example, "for every $y$ there is an $x$ such that $x^2 + y \leq 3$." Is that statement true or false?
• Tarski's theorem (1951) proved this is always decidable: an algorithm exists that settles any such statement about the real numbers. But Tarski's original method was so slow it was useless in practice.
• Collins' CAD (1975) gave a real algorithm: build the sign-invariant cells for all the polynomials involved, then just check which cells make the formula true. Because the truth value of a polynomial inequality never changes inside a cell, checking becomes finite bookkeeping instead of an infinite search over real numbers.
• The cost: the number of cells can grow doubly exponentially in the number of variables — roughly $2^{2^{n}}$ in the worst case for $n$ variables. Two polynomials in the plane are cheap, as our demo shows; a dozen polynomials in ten variables can be far beyond what any computer will ever finish.

So CAD is a genuine triumph: it proves the theory of the reals is decidable, something that fails for the integers (Gödel's incompleteness territory). But decidable does not mean fast — CAD sits among the problems whose worst case is provably enormous, a very concrete face of the gap explored in P vs NP.

Any time a problem can be phrased as "for which values does this system of polynomial constraints hold," CAD or one of its descendants is a candidate tool:

• Robot motion planning: describing the free space a robotic arm can reach without collision is naturally a system of polynomial inequalities in the joint angles.
• Control theory: proving a controller keeps a system stable for every parameter in some range is a $\forall$-quantified polynomial statement — exactly CAD's home turf.
• Automated theorem proving: computer algebra systems use CAD to settle geometric conjectures and algebraic inequalities automatically, no human proof required.
• SMT solvers for nonlinear arithmetic: modern software verification tools call CAD-based procedures whenever a formula mixes real variables with polynomial constraints, extending the reach of SAT-style solving to curved, nonlinear worlds.

Anywhere reasoning must cross from "some example works" to "it works for every real number in this range," CAD is the classical way to make that leap rigorous and mechanical.

Cylindrical Algebraic Decomposition takes an infinite question — "is this true for all real numbers?" — and answers it with a finite map: a set of cells where nothing about your polynomials' signs can ever surprise you. That map is what makes George Collins' 1975 algorithm a genuine decision procedure for the reals, forty years after Tarski proved one had to exist.

The price of that certainty is steep — cell counts that can explode doubly exponentially — but the shape of the idea is a small miracle: geometry tamed into a lookup table. The next time a solver certifies that a controller is stable for every possible parameter, or that a robot arm truly cannot collide, there is a good chance a decomposition much like this one is quietly doing the work.