Feasibility via quantifier elimination

Consider the system of polynomial equations and inequalities [1]

$\begin{array}{rrl} f_1 (x_1, x_2) :=& x_1^2 + x_2^2 - 1 &= 0\\ g_1 (x_1, x_2) :=& 3 x_2 - x_1^3 - 2 &\geq 0\\ g_2 (x_1, x_2) :=& x_1 - 8 x_2^3 &\geq 0\end{array}$

whose solution set is the following semialgebraic set

$S := \{ (x_1,x_2) \in \mathbb{R}^2 \mid f_1 (x_1,x_2) = 0 \land g_1 (x_1,x_2) \geq 0 \land g_2 (x_1,x_2) \geq 0\}$

Parrilo showed in [1] that this system is infeasible, i.e., set $S$ is empty, using the Positivstellensatz [2]. Alternatively, one could use quantifier elimination to conclude infeasibility.

Consider the following proposition

$\exists{x_1}\exists{x_2} \left(f_1 (x_1,x_2) = 0 \land g_1 (x_1,x_2) \geq 0 \land g_2 (x_1,x_2) \geq 0\right)$ .

If this proposition is true, then the system is feasible and $S$ is nonempty. If the proposition is false, then the system is infeasible and $S$ is empty. We can determine the truth value of the proposition using REDUCE + REDLOG to perform quantifier elimination:

% feasibility via quantifier elimination

load_package redlog;
rlset ofsf;

% define polynomial functions
f1 := x1^2+x2^2-1;
g1 := 3*x2-x1^3-2;
g2 := x1-8*x2^3;

% define existential formula
phi := ex({x1,x2}, f1=0 and g1>=0 and g2>=0);

% perform quantifier elimination
rlqe phi;

end;

The output of this script is the following:

The proposition is false and, thus, the system is infeasible.

__________

References

[1] Pablo Parrilo, Sum of Squares Programs and Polynomial Inequalities.

[2] Jacek Bochnak, Michel Coste, Marie-Françoise Roy, Real Algebraic Geometry, Springer, 1998.

About these ads

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

This entry was posted on August 27, 2011 at 18:24 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

Like this:

Leave a Reply Cancel reply

Follow “Rod Carvalho”