(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 ].

======================================================= 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 ] ] =======================================================

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 Last modified: Tue Jul 30 17:29:21 EDT 2002