## 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

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.