Q E P C A D -Testing Positive SemiDefiniteness

Background

In "An effective decision method for semidefinite polynomials", Zeng Guangxing and Zeng Xiaoning, Journal of Symbolic Computation 37 (2004) pages 83-99, the authors give a special-purpose algorithm for deciding the semidefiniteness of multivariate polynomials and for providing witness points for polynomials that aren't semidefinite. Here we consider how best to answer such questions with QEPCAD, and try QEPCAD out on one of their examples.

Formulating the problem for QEPCAD

The striaghtforward translation of "is p positive semidefinite" into quantifier elimination is "∀ x1, x2, ..., xn [ p(x1,...,xn) >= 0 ]". However, this is not a very efficient formulation for QEPCAD. If p fails to be positive semidefinite, there must be an open set of points on which p < 0. So we can phrase our problem as the "not" of

(F x1)(F x2)...(F xn)[ p(x1,...,xn) < 0 ]

where, recall, "F" means "there exist infinitely many". Clearly if this formula is true p is not semi-definite. After all, it would have been enough to find one point at which p is negative and we would have found infinitely many. However, what if this formula returns false? Is it possible that p could none-the-less not be positive semi-definite? No, because if p is not positive semi-definite there is an open set of points in which p < 0, and this open set provides infinitely many values of x1 such that there are infinitely many values of x2 such that ... such that there are inifinitely many values of xn such that p(x1,...,xn) < 0.

Why is this formulation better? Intuituvely, deciding "there exists infinitely many x" is easier because you can miss or ignore finitely many values of x and you'll still get the right answer. In QEPCAD's case, it chooses to ignore the finitely many test values it has for x that not rational. This way it doesn't have to do algebraic number computations and that's a HUGE win in terms of performance.

The Example Problem

Number 4 of Guangxing and Xiaoning "Examples of quaternary [i.e. 4-variate] polynomials" is:

p = w^6 + 2 z^2 w^3 + x^4 + y^4 + z^4 + 2 x^2 w + 2 x^2 z + 3 x^2 + w^2 + 2 z w + z^2 + 2 z + 2 w + 1

CAD construction is very sensitive to variable ordering, and this example demonstrates that well. As a general rule of thumb when producing a CAD for a single polynomial try to order variables in

1. Descending order by degree of variable, breaking ties with
2. Descending order by highest total-degree term in which the variable appears, breaking ties with
3. Descending order by number of terms containing the variable

When the input contains many polynomials hueristics for variable ordering become more complicated. In this case, p is degree 6 in w and degree 4 in the rest, so our order starts as (w,...). Amongst the remaining variables, z appears in a total degree 5 term, and the rest appear in terms of total degree at most 4, giving us (w,z,...). Amongst x and y, x appears in more terms, so we end up with (w,z,x,y) as a variable ordering.

The following QEPCAD session, run on a ??? MHz Pentium IV with ??? MB RAM, shows that p is in fact positive semidefinite. QEPCAD was run with the default size for Saclib's garbage collected space, which is 2MB, and required 0.15 seconds of CPU time to produce its result.

=======================================================
                Quantifier Elimination                 
                          in                           
            Elementary Algebra and Geometry            
                          by                           
      Partial Cylindrical Algebraic Decomposition      
                                                       
               Version B 1.30, 05 Feb 2004
                                                       
                          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 Robidoux, and Stanly Steinberg                 
=======================================================
Enter an informal description  between '[' and ']':
[ Computes the "not" of "is p positive semidefinite?" ]
Enter a variable list:
(w,z,x,y)
Enter the number of free variables:
0
Enter a prenex formula:
(F w)(F z)(F x)(F y)[
w^6 + 2 z^2 w^3 + x^4 + y^4 + z^4 + 2 x^2 w + 
2 x^2 z + 3 x^2 + w^2 + 2 z w + z^2 + 2 z + 2 w + 1 < 0
].


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

Before Normalization >
finish

An equivalent quantifier-free formula:

FALSE


=====================  The End  =======================

-----------------------------------------------------------------------------
1 Garbage collections, 492023 Cells and 0 Arrays reclaimed, in 20 milliseconds.
411729 Cells in AVAIL, 500000 Cells in SPACE.

System time: 150 milliseconds.
System time after the initialization: 140 milliseconds.
-----------------------------------------------------------------------------