Feasibility via quantifier elimination II

Suppose we want to decide whether the following semialgebraic set

$S := \{(x,y) \in \mathbb{R}^2 \mid x - y^2 + 1 \geq 0 \land -x - y^2 + 1 \geq 0\}$

is nonempty. This is the same as determining whether the following system of polynomial inequalities

$\begin{array}{rrl} g_1 (x, y) :=& x - y^2 + 1 &\geq 0\\ g_2 (x, y) :=& -x - y^2 +1 &\geq 0\end{array}$

is feasible. We now define $S_1 := \{(x,y) \in \mathbb{R}^2 \mid g_1 (x, y) \geq 0\}$ , and $S_2 := \{(x,y) \in \mathbb{R}^2 \mid g_2 (x, y) \geq 0\}$ . Set $S_1$ is depicted below

and set $S_2$ is depicted below

Note that $S = S_1 \cap S_2$ . We depict this intersection below

Visual inspection of the plot of the intersection $S = S_1 \cap S_2$ allows us to conclude that $S$ in nonempty. Asserting that $S$ is nonempty is the same as stating that the proposition

$\exists{x}\exists{y} \left(g_1 (x,y) \geq 0 \land g_2 (x,y) \geq 0\right)$

is true. We can determine the truth value of this proposition via quantifier elimination using the following REDUCE + REDLOG script:

% feasibility via quantifier elimination

load_package redlog;
rlset ofsf;

% define polynomial functions
g1 :=  x-y^2+1;
g2 := -x-y^2+1;

% define existential formula
phi := ex({x,y}, g1>=0 and g2>=0);

% perform quantifier elimination
rlqe phi;

end;

which produces the truth value true. This means that there exists a $(x,y)$ that satisfies the polynomial inequalities, i.e., $S$ is nonempty.

__________

Remark: the plots in this post were generated by Wolfram Alpha.

About these ads

Tags: Decision Problems, Feasibility, Quantifier Elimination, Real Algebraic Geometry, REDLOG, REDUCE, Semialgebraic Geometry, Semialgebraic Sets

This entry was posted on August 29, 2011 at 00:47 and is filed under Algebraic Geometry. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Rod Carvalho

Feasibility via quantifier elimination II

Like this:

Leave a Reply Cancel reply

Follow “Rod Carvalho”