Deciding the convexity of semialgebraic sets

Given a basic closed semialgebraic set [1], , defined by

where and , how can one decide if set is convex? Can one use quantifier elimination?

__________

Convexity

Let us recall the definition of convexity [2]:

Definition: A set is convex if the line segment between any two points in lies in , i.e., if for any and any with , we have .

Let us introduce a predicate , defined by

so that we can write in the more parsimonious form

.

Hence, writing is equivalent to asserting that . From the definition above, it follows that set is convex if and only if the following universally quantified formula

where range over and ranges over , evaluates to . Since are polynomials, the formula above can be decided using quantifier elimination software like QEPCAD or REDLOG. Unfortunately, decidability does not imply that real quantifier elimination will decide the formula in an expedite manner. Let us now consider two instances of the decision problem under study.

__________

Example #1

Consider the following semialgebraic set

which we depict below

Visual inspection of the plot above allows us to conclude that set is convex. However, relying on the human visual system is extremely limiting. Therefore, we would like to automate the decision. We decide the convexity of via quantifier elimination using the following REDUCE + REDLOG script:

% decide the convexity of a semialgebraic set

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (x1-x2^2+3>=0) and (-x1-x2^2+3>=0);
p2 := (y1-y2^2+3>=0) and (-y1-y2^2+3>=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  := (z1-z2^2+3>=0) and (-z1-z2^2+3>=0); 

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

% perform quantifier elimination
rlqe phi;

end;

This script returns the truth value and, hence, is, indeed, convex. However, it took REDLOG approximately 60 seconds to decide the convexity of , which is considerably longer than any of my previous experiments with REDLOG. Since we are performing quantifier elimination on a formula with five universal quantifiers, I am not incredibly surprised that it takes a while to obtain an answer.

__________

Example #2

Consider now the following semialgebraic set

part of which we depict below

Visual inspection of the plot above allows us to conclude that set is not convex. We decide the convexity of using the following REDUCE + REDLOG script:

% decide the convexity of a semialgebraic set

load_package redlog;
rlset ofsf;

% define predicates in antecedent
p1 := (x1-x2^2+3>=0) and (x1-x2^2+1<=0);
p2 := (y1-y2^2+3>=0) and (y1-y2^2+1<=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  := (z1-z2^2+3>=0) and (z1-z2^2+1<=0); 

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

% perform quantifier elimination
rlqe phi;

end;

This script returns the truth value and, hence, is, indeed, not convex. Interestingly, it took REDLOG less than one second to decide the formula. That is over two orders of magnitude faster than in example #1.

__________

References

[1] Markus Schweighofer, Describing convex semialgebraic sets by linear matrix inequalities, International Symposium on Symbolic and Algebraic Computation, Korea Institute for Advanced Study, Seoul, July 2009.

[2] Stephen Boyd, Lieven Vandenberghe, Convex Optimization.