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.
Tags: Convex Algebraic Geometry, Convexity, Decision Problems, Quantifier Elimination, Real Algebraic Geometry, REDLOG, REDUCE, Semialgebraic Geometry, Semialgebraic Sets

