Deciding the convexity of semialgebraic sets II

Let S_3 \subset \mathbb{R}^{3 \times 3} denote the set of real symmetric 3 \times 3 matrices. We introduce a matrix-valued function A: \mathbb{R}^3 \to S_3 defined by

A (x) = \left[\begin{array}{ccc} 1 & x_1 & x_2\\ x_1 & 1 & x_3\\ x_2 & x_3 & 1\end{array}\right]

The elliptope E_3 \subset \mathbb{R}^3 is defined by

E_3 = \left\{ x \in \mathbb{R}^3 \mid A (x) \succeq 0 \right\}

where A (x) \succeq 0 means that matrix A (x) is positive semidefinite. Since the elliptope E_3 is defined by the linear matrix inequality (LMI) A (x) \succeq 0, we can conclude that E_3 is a spectrahedron and, therefore, we have that E_3 is convex.

The E_3 elliptope (also known as “inflated tetrahedron”) is the yellow part (surface and interior) of the Cayley’s cubic surface plotted below

[ source ]

__________

E_3 is a semialgebraic set

Saying that A (x) is positive semidefinite is equivalent to saying that the 2^3 - 1 = 7 principal minors of A (x) are nonnegative. If A (x) \succeq 0, then the three 1st order principal minors (which are the diagonal entries of A (x)) lead to the following three (admittedly uninteresting) inequalities

1 \geq 0,     1 \geq 0,     1 \geq 0

which we can discard. The three 2nd order principal minors (determinants of 2 \times 2 submatrices of A (x)) and the 3rd order principal minor (the determinant of A (x)) can be computed using the following Python 2.5 + SymPy script:

from sympy import *

# symbolic variables
x1 = Symbol('x1')
x2 = Symbol('x2')
x3 = Symbol('x3')

# build matrix A(x)
A = Matrix([[1,x1,x2],
            [x1,1,x3],
            [x2,x3,1]])

print "\nMatrix A(x):"
print A

print "\n2nd order principal minors:"
print A.extract([0,1],[0,1]).det()
print A.extract([0,2],[0,2]).det()
print A.extract([1,2],[1,2]).det()

print "\n3rd order principal minor:"
print A.det()

which produces the following output:

Matrix A(x):
[ 1, x1, x2]
[x1,  1, x3]
[x2, x3,  1]

2nd order principal minors:
-x1**2 + 1
-x2**2 + 1
-x3**2 + 1

3rd order principal minor:
-x1**2 + 2*x1*x2*x3 - x2**2 - x3**2 + 1

Hence, the 2nd order principal minors yield the following inequalities

1 - x_1^2 \geq 0,     1 - x_2^2 \geq 0,     1 - x_3^2 \geq 0

which define the 3-dimensional cube [-1,1]^3 \subset \mathbb{R}^3. The 3rd order principal minor (i.e., the determinant) yields the inequality

1 + 2 x_1 x_2 x_3 - (x_1^2 + x_2^2 + x_3^3) \geq 0.

We can thus conclude that E_3 is a basic closed semialgebraic set.

__________

Deciding the convexity of E_3

In my last post, I used quantifier elimination to decide the convexity of two semialgebraic sets in \mathbb{R}^2. Let us now decide the convexity of E_3, which is of higher “complexity” than the sets I considered last time. What is the goal? The goal is to find out whether REDLOG can decide the convexity of E_3 in less than 10 minutes.

Based on the scripts in my previous post, we write the following REDUCE + REDLOG script to decide the convexity of E_3:

% decide the convexity of the elliptope E3

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (1-x1^2>=0) and (1-x2^2>=0) and (1-x3^2>=0) and 
      (1-x1^2-x2^2-x3^2+2*x1*x2*x3>=0);
p2 := (1-y1^2>=0) and (1-y2^2>=0) and (1-y3^2>=0) and 
      (1-y1^2-y2^2-y3^2+2*y1*y2*y3>=0);
p3 := (theta>=0) and (theta<=1);

% define predicate in the consequent
z1 := theta*x1+(1-theta)*y1;
z2 := theta*x2+(1-theta)*y2;
q  := (1-z1^2>=0) and (1-z2^2>=0) and (1-z3^2>=0) and 
      (1-z1^2-z2^2-z3^2+2*z1*z2*z3>=0);

% define universal formula
phi := all({x1,x2,x3,y1,y2,y3,theta}, (p1 and p2 and p3) impl q);

% perform quantifier elimination
rlqe phi;

end;

After 30 minutes (!!!) waiting for the decision procedure to terminate, I killed the reduce.exe process (which was eating all my machine’s CPU cycles and RAM memory). This is disappointing…

About these ads

Tags: , , , , , , , , , , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Connecting to %s


Follow

Get every new post delivered to your Inbox.

Join 76 other followers

%d bloggers like this: