# Q E P C A D - Example: Hong,
Liska, Steinberg 5.14

This example problem is formula 5.14 from Hong, Liska, Steinberg,
"Testing Stability by Quantifier Elimination", Journal of Symbolic
Computation, Vol. 24, No. 2, August 1997. They report that QEPCAD
was unable to prove 5.14 true (meaning the time or space resources
were prohibitive). Here we show how we used the
current version of QEPCAD and some tricks to prove formula 5.14
true in less than 2 seconds on a 800Mhz P3 laptop.

## The Problem

The problem we consider here is:
F1 (formula 5.14 from the article) =
(A a)(A b)(A c2)[ [0 <= a <= 1 /\ 0 <= b <= 1] ==> A <= 0 /\ C <= 0 /\ [D <= 0 \/ B <= 0] ]

where A, B, C, and D are polynomials in a,b, and c2.
A = c2^4 (a - b + 1) ( a - b - 1) (a - b)^2
B = 2 c2^4 b ( 3 a^2 b - 2 a^2 - 2 a b^2 + a + b^3 - b)
+ 4 c2^3 a b ( a^2 - a + b^2 - b)
+ 2 c2^2 a ( a^3 - 2 a^2b + 3 a b^2 - a - 2 b^2 + b )
C = c2^4 b^2 (b^2 - 1) + 4 c2^3 a b^2 (b - 1)
+ 2 c2^2 a b (3 a b - 2 a - 2 b + 1)
+ 4 c2 a^2 b (a - 1) + a^2 (a^2 - 1)
D = c2^2 ( 8 a^2 b^2 - 12 a^2 b + 5 a^2 - 8 a b^3 + 8 a b^2
+ 2 a b - 4 a + 4 b^4 - 4 b^3 - 3 b^2 + 4 b )
+ 2 c2 ( 4 a^3 b - 2 a^3 - 4 a^2 b^2 - 2 a^2 b + a^2
+ 4 a b^3 - 2 a b^2 + 2 a b - 2 b^3 + b^2 )
+ 4 a^4 - 8 a^3 b - 4 a^3 + 8 a^2 b^2 + 8 a^2 b - 3 a^2
- 12 a b^2 + 2 a b + 4 a + 5 b^2 - 4 b

## The Solution

Notice that all the inequalities in the formula are non-strict.
This means that any point at which the quantifier-free part of the
formula is not satisfied is surrounded by a nieghborhood of points
at which the quantifier-free part of the formula is not satisfied.
All quantifiers are "for all", which means we're searching for
counter-examples. By the above argument, we're searching for open
sets of counter-examples. Thus, we can replace each of the "for all"
quantifiers in the original formula with the "for all but
finitely many" quantifier (which is `G`

for
"generic" in QEPCAD B) and
produce an equivalent formula.
QEPCAD B is able to return "true" for this formulation in about 2
seconds on my 800Mhz P3 laptop. See the
QEPCADB input.
The moral of the story is this: "for all but finitely many" can
be decided using CAD faster than "for all" (which makes sense,
since finitely many points can be ignored), so you should use it
if you can. Note, however, that it doesn't make a difference with
the top-level quantifier.

## Last Remark (and a pretty picture)

I wondered what the projection of
`A <= 0 /\ C <= 0 /\ [D <= 0 \/ B <= 0] ]`

onto the a-b plane looks like. So here it
is (the unit grid is shown in green, and the coordinate axes
in red) at least up to some lower dimensional subset. It's a
bizarre picture when you think about it. These polynomials just
happen to intersect along a couple of planes that are nicely
algined with the coordinate axes.
Here only one quantifier was eliminated, so the
`G`

quantifier doesn't help us. However,
QEPCAD B is able to compute adjacencies between cells in a CAD
of 2-space, and has a command called `tvc2d`

(which stands for "truth value closure 2D") that completes truth
value assignments to cells of a CAD of 2-space based on the
assumption that the solution set is the closure of an open set,
which should be the case for this problem. So, I instructed
QEPCADB to lift over cells in 2-space only when they had full
dimension, and used tvc2d to assign truth values to the lower
dimensional cells. See the
QEPCADB input

Christopher W Brown
Last modified: Wed Aug 13 10:10:26 EDT 2003