CAD
Published:
Long ago I was amazed to read Zeilberger’s A = B, a masterpiece on proving binomial coefficient identities, and have ever since been surprised that more people don’t know about it. I recently had this feeling again while reading Kauers’ overview of the cylindrical algebraic decomposition algorithm (CAD).
The sales pitch is this: There exists an algorithm that can determine whether any firstorder statement about the reals involving polynomial equations and inequalities is true or false. The precise statement is more technical, but that’s the idea^{1}. Apparently we’ve known that this algorithm has existed since the 1960’s, and have had an effective implementation since the 1970’s. Well, it was news to me!
There are lots of silly examples I could give, but let me just dive into a real, recent problem I was thinking about.
For which integers $a$ and $b$ does the cubic
\[\begin{align*} f(s, t) = 1  2 a s &+ a^2 s^2  b s^2 + s^3 + a b s^3  b t \\ & 3 s t + a b s t + a s^2 t + b^2 s^2 t + a t^2 + 2 b s t^2 + t^3 \end{align*}\]have a positive minimum on the region $\{a s + bt \geq 1\} \cap [0, 1]^2$?
This is an annoying problem. I solved it using computer algebra to automate my calculusbased analysis, but I didn’t get an answer I was happy with. CAD can do it almost automatically!
We can phrase our question like this: For which $a, b$ does the formula
\[\forall s, t\ [0 \leq s, t \leq 1,\ as + bt \geq 1 \implies f(s, t) > 0]\]hold? (Note that we don’t need another variable for the minimum itself. The region is compact, so $f(s, t) > 0$ is enough.) If we give this statement to a CAD algorithm, then it will turn it into an unquantified statement, meaning that it only depends on $a$ and $b$. Here’s what Mathematica’s built in CAD does:
f = 1  2 a s + a^2 s^2  b s^2 + s^3 + a b s^3  b t  3 s t + a b s t + a s^2 t + b^2 s^2 t + a t^2 + 2 b s t^2 + t^3
CylindricalDecomposition[
ForAll[{s, t},
Implies[0 <= s <= 1 && 0 <= t <= 1 && a*s + b*t >= 1, f > 0]],
{b, a}]
(b <= (17/4) && (a < (2  b)/2  1/2 Sqrt[4 + b^2]  a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 3]))
 ((17/4) < b <= 2 && (a < (2  b)/2  1/2 Sqrt[4 + b^2]  a > (2  b)/2 + 1/2 Sqrt[4 + b^2]))
 2 < b < 1
 (1 <= b < 2.08... && a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 1])
 (b == 2.08... && a > (2  b)/2 + 1/2 Sqrt[4 + b^2])
 (b > 2.08... && a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 1])
The output is a disjoint union of conditions which, together, are equivalent to our input. The full output is a bit messy, so here it is again with only the parts relevant to “integers $b \geq 1$”:
(1 <= b < 2.08... && a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 1])
 (b > 2.08... && a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 1])
And now, noticing that the inner condition on $a$ is the same in both clauses, and that we only care about integer values, we see that this whole thing is equivalent to just this:
a > Root[27  4 b^3 + 18 b #1  b^2 #1^2 + 4 #1^3 &, 1]
This says that our original statement about $f$ is equivalent to “$a$ is larger than the smallest root $x$ of the cubic $27  4 b^3 + 18 b x  b^2 x^2 + 4 x^3$.” This sounds unhelpful, but it is actually quite strong.
Using CAD again, we can determine when this cubic has only one real root. Because it’s a cubic, this is the negation of the statement
\[\exists x < y < z \ [q(x) = q(y) = q(z) = 0],\]where $q$ is the cubic in question. Let’s pass that to Mathematica:
q = 27  4 b^3 + 18 b x  b^2 x^2 + 4 x^3
CylindricalDecomposition[
Exists[{x, y, z},
x < y < z &&
q == 0 && (q /. {x > y}) == 0 && (x /. {x > z}) == 0], {b}]
b < 1.89...
If $b > 1$ (we only care about integers), then the cubic only has one root. In that case, because its leading coefficient in $x$ is positive, being larger than the real root is equivalent to saying that the cubic is positive. If $b = 1$, then we can just do CAD again but substitute $b = 1$ first, which reveals that the condition is $a > 1$.
So, all together, we have this: If $b = 1$, then $f(s, t) > 0$ on the region for all positive integers $a$; if $b \geq 2$, then $f(s, t) > 0$ on the region if and only if
\[27 + 4 a^3 + 18 a b  a^2 b^2  4 b^3 > 0.\]This is the very precise, quantitative statement I wanted all along, and it only took a few minutes of computing time (plus some more exploring) to discover. Amazing!

And even this pitch lowballs CAD. If you get into the underlying geometry, what CAD computes tells you more than whether particular firstorder statements are true. ↩