# Q E P C A D - Edge Square Product Example

Using easy eliminations before calling QEPCAD, declaring an equational contraint, using topological information in 2D.

```(E x1)(E x2)(E y2)[
x = x1 x2 - y2 /\
y = x1 y2 + x2 /\
0 <= x1 /\ x1 <= 2 /\
2 <= x2 /\ x2 <= 4 /\
-1 <= y2 /\ y2 <= 1
].
```
This example is due to George E. Collins. It asks for the "complex product" of a square and a segment in the complex plane. The segment is [0,2]x{1} and the square is [2,4]x[-1,1]. Probably the obvious way to phrase this as a QE problem is what you see in the first screen: x and y are set to the real and imaginary parts of the complex product of x1 + i and x2 + i y2, x1 + i being a point on the segment and x2 + i y2 being a point in the square. However, with this formulation of the problem QEPCAD takes a prohibative amount of memory, and with enough memory the time would be prohibative.

```=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition

Version B 0.1, 30 Jul 2002

by
Hoon Hong
(hhong@math.ncsu.edu)

With contributions by: Christopher W. Brown, George E.
Collins, Mark J. Encarnacion, Jeremy R. Johnson
Werner Krandick, Richard Liska, Scott McCallum,
Nicolas Robiduex, and Stanly Steinberg
=======================================================
Enter an informal description  between '[' and ']':
[
Edge-square product problem with equational constaints
]
Enter a variable list:
(x,y,x1,x2)
Enter the number of free variables:
2
Enter a prenex formula:
(E x1)(E x2)[
y = x1 (x1 x2 - x) + x2 /\
0 <= x1 /\ x1 <= 2 /\
2 <= x2 /\ x2 <= 4 /\
-1 <= (x1 x2 - x) /\ (x1 x2 - x) <= 1
].

=======================================================

Before Normalization >
prop-eqn-const

Before Normalization >
go

Before Projection (x2) >
d-level-f 4
A_4,1  = input
= x1^2 x2 + x2 - x x1 - y
A_4,2  = input
= x2 - 2
A_4,3  = input
= x2 - 4
A_4,4  = input
= x1 x2 - x + 1
A_4,5  = input
= x1 x2 - x - 1

Before Projection (x2) >
eqn-const-l (A_4,1)

Before Projection (x2) >
finish
An equivalent quantifier-free formula:

x + 1 >= 0 /\ y + 2 x - 20 <= 0 /\ 2 y - x + 5 >= 0 /\
8 y + x^2 - 16 >= 0 /\ 4 y - x - 17 <= 0 /\
[ 2 y + x - 5 >= 0 \/ y - 2 >= 0 \/ [ x - 1 >= 0 /\
x - 2 <= 0 ] \/ [ x - 1 <= 0 /\ x >= 0 ] ]
=======================================================
```
However, it's easy to see from the first equality that y2 = x1 x2 - x, so we can substitute x1 x2 - x for y in the formula and eliminate one variable before we even start. This yields a second input formula, which is quite a bit better for QEPCAD than the first. We can solve for x2 using the second equation, but doing so gives us the substitution x2 = (y + x)/(x1^2 + 1), which has a denominator. We could still make the substitution and then clear denominators, but there is another more general solution using QEPCAD: the remaining equation may be declared as an equational constraint (documentation on equational constraints). Equational constraints must be used with care, but if there is a polynomial of the higest level that must be zero for the quantifier-free part of the input formula to be true, it may be declared an equational contraint. The second screen shows the QEPCAD session that realizes this input formulation. In general, only one projection factor may be declared an equational constraint, although QEPCAD does not enforce this.

In this form, QEPCAD solves the Edge-Square Product in 80 seconds on my Sun Ultra 60. There is, however, an even fast way to arrive at the solution. It can be proven that the answer to this problem must be a set that is the closure of an open set. QEPCAD is able to take a partial assignment of truth values to cells in a CAD of 2-space and deduce other truth values given that the set to be represeted is the closure of an open set. Here's what the input to QEPCAD would look like:

```[]
(x,y,x1,x2)
2
(E x1)(E x2)[
y = x1 (x1 x2 - x) + x2 /\
0 <= x1 /\ x1 <= 2 /\
2 <= x2 /\ x2 <= 4 /\
-1 <= x1 x2 - x /\ x1 x2 - x <= 1
].
prop-eqn-const
go
eqn-const-l (A_4,1)
go
sel [level = dimension \/ level > 2 ]
go
sel [level < 2 ]
go
tvc2d
use-sel n
go
sol T
d-stat
```

Christopher W Brown