Introduction

Draw the curve x2+y2−4=0x^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.

Try It

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

<p class="hint">Two fixed polynomials live on this plane: <b>f(x,y) = x&sup2; + y&sup2; - 4</b> (a circle) and <b>g(x,y) = y - x&sup2;</b> (a parabola). Press <b>Decompose</b> to shade every point by the sign pattern of (f, g).</p>
<div class="stage">
  <canvas id="board" width="360" height="360"></canvas>
  <div class="legend">
    <div class="row"><span class="swatch pp"></span>f > 0, g > 0</div>
    <div class="row"><span class="swatch pm"></span>f > 0, g < 0</div>
    <div class="row"><span class="swatch mp"></span>f < 0, g > 0</div>
    <div class="row"><span class="swatch mm"></span>f < 0, g < 0</div>
    <div class="row"><span class="swatch curve"></span>f = 0 or g = 0 (cell boundary)</div>
  </div>
</div>
<div class="status" id="status">Press Decompose to build the sign-invariant map.</div>
<div class="btns">
  <button id="decompose" type="button">Decompose</button>
  <button id="reset" type="button" class="ghost">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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Cylindrical algebraic decomposition demo: shade the plane by the sign pattern of two fixed polynomials.
// f(x,y) = x^2 + y^2 - 4 (circle of radius 2), g(x,y) = y - x^2 (parabola).
const W = 360, H = 360, N = 90;
const RANGE = 3.2; // half-width of the world-coordinate window shown on screen

// Convert a pixel coordinate on the canvas into world (x,y) coordinates.
function toWorld(px, py) {
  return [ (px / W) * (2 * RANGE) - RANGE, RANGE - (py / H) * (2 * RANGE) ];
}

// f(x,y): negative inside the circle of radius 2, positive outside, zero on it.
function f(x, y) { return x * x + y * y - 4; }
// g(x,y): negative below the parabola y = x^2, positive above, zero on it.
function g(x, y) { return y - x * x; }

const canvas = document.getElementById('board');
const ctx = canvas.getContext('2d');
let decomposed = false;

// One color per sign combination of (f, g); curves (sign = 0) get their own color.
const COLORS = { '1,1': '#cdeccd', '1,-1': '#f6d6a6', '-1,1': '#a9d3f2', '-1,-1': '#e3b8d6' };
const CURVE = '#1d3557';
const EPS = 0.05;

function sign(v) { return Math.abs(v) < EPS ? 0 : (v > 0 ? 1 : -1); }

function drawBlank() {
  ctx.fillStyle = '#fff';
  ctx.fillRect(0, 0, W, H);
  ctx.strokeStyle = '#e3e8ee';
  for (let i = 0; i <= 8; i++) {
    const p = (i / 8) * W;
    ctx.beginPath(); ctx.moveTo(p, 0); ctx.lineTo(p, H); ctx.stroke();
    ctx.beginPath(); ctx.moveTo(0, p); ctx.lineTo(W, p); ctx.stroke();
  }
}

// Scan a fine grid and paint each sample by its sign pattern — approximates the true CAD cells.
function decompose() {
  const cell = W / N;
  for (let i = 0; i < N; i++) {
    for (let j = 0; j < N; j++) {
      const px = (i + 0.5) * cell, py = (j + 0.5) * cell;
      const [x, y] = toWorld(px, py);
      const sf = sign(f(x, y)), sg = sign(g(x, y));
      if (sf === 0 || sg === 0) {
        ctx.fillStyle = CURVE;
      } else {
        ctx.fillStyle = COLORS[sf + ',' + sg];
      }
      ctx.fillRect(i * cell, j * cell, cell + 0.6, cell + 0.6);
    }
  }
  decomposed = true;
  setStatus('Decomposed. Click any cell to inspect its sign pattern.');
}

function setStatus(t) { document.getElementById('status').textContent = t; }

canvas.addEventListener('click', (ev) => {
  if (!decomposed) return;
  const rect = canvas.getBoundingClientRect();
  const px = (ev.clientX - rect.left) * (W / rect.width);
  const py = (ev.clientY - rect.top) * (H / rect.height);
  const [x, y] = toWorld(px, py);
  const sf = sign(f(x, y)), sg = sign(g(x, y));
  // Report the sign pattern of the polynomials at the clicked point.
  setStatus(i18nFmt('At (%x%, %y%): sign(f) = %fs%, sign(g) = %gs% — constant throughout this cell.', { fs: sf, gs: sg, x: x.toFixed(2), y: y.toFixed(2) }));
  console.log('Sign pattern at clicked point:', 'x=', x.toFixed(2), 'y=', y.toFixed(2), 'sign(f)=', sf, 'sign(g)=', sg);
});

document.getElementById('decompose').addEventListener('click', decompose);
document.getElementById('reset').addEventListener('click', () => {
  decomposed = false;
  drawBlank();
  setStatus('Press Decompose to build the sign-invariant map.');
});

drawBlank();
Result
Console

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.

The Real Complexity

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 yy there is an xx such that x2+y≤3x^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 22n2^{2^{n}} in the worst case for nn 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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/cylindrical-algebraic-decomposition/Content licensed under CC BY-NC 4.0.