## Posts Tagged ‘Quantifier Elimination’

### Deciding the convexity of semialgebraic sets II

June 23, 2012

Let $S_3 \subset \mathbb{R}^{3 \times 3}$ denote the set of real symmetric $3 \times 3$ matrices. We introduce a matrix-valued function $A: \mathbb{R}^3 \to S_3$ defined by

$A (x) = \left[\begin{array}{ccc} 1 & x_1 & x_2\\ x_1 & 1 & x_3\\ x_2 & x_3 & 1\end{array}\right]$

The elliptope $E_3 \subset \mathbb{R}^3$ is defined by

$E_3 = \left\{ x \in \mathbb{R}^3 \mid A (x) \succeq 0 \right\}$

where $A (x) \succeq 0$ means that matrix $A (x)$ is positive semidefinite. Since the elliptope $E_3$ is defined by the linear matrix inequality (LMI) $A (x) \succeq 0$, we can conclude that $E_3$ is a spectrahedron and, therefore, we have that $E_3$ is convex.

The $E_3$ elliptope (also known as “inflated tetrahedron”) is the yellow part (surface and interior) of the Cayley’s cubic surface plotted below

[ source ]

__________

$E_3$ is a semialgebraic set

Saying that $A (x)$ is positive semidefinite is equivalent to saying that the $2^3 - 1 = 7$ principal minors of $A (x)$ are nonnegative. If $A (x) \succeq 0$, then the three 1st order principal minors (which are the diagonal entries of $A (x)$) lead to the following three (admittedly uninteresting) inequalities

$1 \geq 0$,     $1 \geq 0$,     $1 \geq 0$

which we can discard. The three 2nd order principal minors (determinants of $2 \times 2$ submatrices of $A (x)$) and the 3rd order principal minor (the determinant of $A (x)$) can be computed using the following Python 2.5 + SymPy script:

from sympy import *

# symbolic variables
x1 = Symbol('x1')
x2 = Symbol('x2')
x3 = Symbol('x3')

# build matrix A(x)
A = Matrix([[1,x1,x2],
[x1,1,x3],
[x2,x3,1]])

print "\nMatrix A(x):"
print A

print "\n2nd order principal minors:"
print A.extract([0,1],[0,1]).det()
print A.extract([0,2],[0,2]).det()
print A.extract([1,2],[1,2]).det()

print "\n3rd order principal minor:"
print A.det()


which produces the following output:

Matrix A(x):
[ 1, x1, x2]
[x1,  1, x3]
[x2, x3,  1]

2nd order principal minors:
-x1**2 + 1
-x2**2 + 1
-x3**2 + 1

3rd order principal minor:
-x1**2 + 2*x1*x2*x3 - x2**2 - x3**2 + 1

Hence, the 2nd order principal minors yield the following inequalities

$1 - x_1^2 \geq 0$,     $1 - x_2^2 \geq 0$,     $1 - x_3^2 \geq 0$

which define the $3$-dimensional cube $[-1,1]^3 \subset \mathbb{R}^3$. The 3rd order principal minor (i.e., the determinant) yields the inequality

$1 + 2 x_1 x_2 x_3 - (x_1^2 + x_2^2 + x_3^3) \geq 0$.

We can thus conclude that $E_3$ is a basic closed semialgebraic set.

__________

Deciding the convexity of $E_3$

In my last post, I used quantifier elimination to decide the convexity of two semialgebraic sets in $\mathbb{R}^2$. Let us now decide the convexity of $E_3$, which is of higher “complexity” than the sets I considered last time. What is the goal? The goal is to find out whether REDLOG can decide the convexity of $E_3$ in less than 10 minutes.

Based on the scripts in my previous post, we write the following REDUCE + REDLOG script to decide the convexity of $E_3$:

% decide the convexity of the elliptope E3

rlset ofsf;

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

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

% perform quantifier elimination
rlqe phi;

end;

After 30 minutes (!!!) waiting for the decision procedure to terminate, I killed the reduce.exe process (which was eating all my machine’s CPU cycles and RAM memory). This is disappointing…

### Deciding the convexity of semialgebraic sets

June 16, 2012

Given a basic closed semialgebraic set [1], $S \subset \mathbb{R}^n$, defined by

$S = \{ x \in \mathbb{R}^n \mid g_1 (x) \geq 0 \land \dots \land g_m (x) \geq 0\}$

where $m \in \mathbb{N}$ and $g_1, \dots, g_m \in \mathbb{R}[x]$, how can one decide if set $S$ is convex? Can one use quantifier elimination?

__________

Convexity

Let us recall the definition of convexity [2]:

Definition: A set $S$ is convex if the line segment between any two points in $S$ lies in $S$, i.e., if for any $x, y \in S$ and any $\theta$ with $0 \leq \theta \leq 1$, we have $\theta x + (1-\theta) y \in S$.

Let us introduce a predicate $p : \mathbb{R}^n \to \{\text{True}, \text{False}\}$, defined by

$\displaystyle p (x) = \bigwedge_{i = 1}^m g_i (x) \geq 0$

so that we can write $S$ in the more parsimonious form

$S = \{ x \in \mathbb{R}^n \mid p (x) \}$.

Hence, writing $x \in S$ is equivalent to asserting that $p (x) = \text{True}$. From the definition above, it follows that set $S$ is convex if and only if the following universally quantified formula

$\forall x \, \forall y \, \forall \theta \, \left[ \, p(x) \land p(y) \land (\theta \geq 0 \land \theta \leq 1) \implies p (\theta x + (1-\theta) y) \, \right]$

where $x, y$ range over $\mathbb{R}^n$ and $\theta$ ranges over $\mathbb{R}$, evaluates to $\text{True}$. Since $g_1, \dots, g_m$ 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

$S_1 := \{ x \in \mathbb{R}^2 \mid x_1 - x_2^2 + 3 \geq 0 \land -x_1 - x_2^2 + 3 \geq 0\}$

which we depict below

Visual inspection of the plot above allows us to conclude that set $S_1$ 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 $S_1$ via quantifier elimination using the following REDUCE + REDLOG script:

% decide the convexity of a semialgebraic set

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 $\text{True}$ and, hence, $S_1$ is, indeed, convex. However, it took REDLOG approximately 60 seconds to decide the convexity of $S_1$, 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

$S_2 := \{ x \in \mathbb{R}^2 \mid x_1 - x_2^2 + 3 \geq 0 \land x_1 - x_2^2 + 1 \leq 0\}$

part of which we depict below

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

% decide the convexity of a semialgebraic set

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 $\text{False}$ and, hence, $S_2$ 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.

### Deciding surjectivity

March 4, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$. We say that $f$ is surjective [1] if and only if for all $y \in \mathcal{Y}$ there exists a $x \in \mathcal{X}$ with $f (x) = y$. More formally, $f$ is surjective if and only if

$\forall y \exists x \left( f (x) = y \right)$

where $x$ and $y$ range over sets $\mathcal{X}$ and $\mathcal{Y}$, respectively. Equivalently, $f$ is surjective if and only if the image of $\mathcal{X}$ under $f$ is $\mathcal{Y}$ itself.

In this post, we will restrict our attention to functions from $\mathbb{R}$ to $\mathbb{R}$. For polynomial functions from reals to reals, we can use quantifier elimination to determine the truth values of the quantified formula above, thus deciding surjectivity.

__________

Example

We would like to decide the surjectivity of the following functions

$\begin{array}{rl} f : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^2\end{array}$                 $\begin{array}{rl} g : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^3\end{array}$

Instead of using the horizontal line test to determine whether these functions are surjective, we use the REDUCE + REDLOG script:

% decide the surjectivity of f(x) = x^2 and g(x) = x^3

rlset ofsf;

% define quantified formulas
phi := all(y, ex(x, x**2=y));
psi := all(y, ex(x, x**3=y));

% perform quantifier elimination
rlqe phi;
rlqe psi;

end;

which decides that $f$ is not surjective and that $g$ is surjective.

__________

References

[1] David Makinson, Sets, Logic and Maths for Computing, Springer, 2008.

### Deciding injectivity

February 28, 2012

Consider a function $f : \mathcal{X} \to \mathcal{Y}$. We say that $f$ is injective if and only if it maps distinct inputs to distinct outputs [1]. More formally, $f$ is injective if and only if

$\forall x_1 \forall x_2 \left( x_1 \neq x_2 \implies f (x_1) \neq f (x_2)\right)$

where $x_1$ and $x_2$ range over set $\mathcal{X}$. Note that the inequations $x_1 \neq x_2$ and $f (x_1) \neq f (x_2)$ are equivalent to $\neg (x_1 = x_2)$ and $\neg \left(f (x_1) = f (x_2)\right)$, respectively. The universally-quantified formula above can be rewritten as follows

$\forall x_1 \forall x_2 \left( \neg (x_1 = x_2) \implies \neg (f (x_1) = f (x_2))\right)$

which looks a bit messy. Contrapositively,

$\forall x_1 \forall x_2 \left( f (x_1) = f (x_2) \implies x_1 = x_2\right)$.

In this post, we will restrict our attention to real-valued functions of a real variable (i.e., functions from $\mathbb{R}$ to $\mathbb{R}$). For polynomial functions from reals to reals, we can use quantifier elimination to determine the truth values of the universally-quantified formulas above, thereby deciding injectivity.

__________

Example

We would like to decide the injectivity of the following functions

$\begin{array}{rl} f : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^2\end{array}$                 $\begin{array}{rl} g : \mathbb{R} &\to \mathbb{R}\\ x &\mapsto x^3\end{array}$

which we plot below (using Wolfram Alpha)

In high school we all learned to use the infamous horizontal line test to determine whether a function is injective. Let us use something more powerful this time, namely, the following REDUCE + REDLOG script:

% decide the injectivity of f(x) = x^2 and g(x) = x^3

rlset ofsf;

% define universally-quantified formulas
phi := all({x1,x2}, x1**2=x2**2 impl x1=x2);
psi := all({x1,x2}, x1**3=x2**3 impl x1=x2);

% perform quantifier elimination
rlqe phi;
rlqe psi;

end;

which decides that $f$ is not injective and that $g$ is injective.

__________

References

[1] David Makinson, Sets, Logic and Maths for Computing, Springer, 2008.

### Deciding the existence of equilibrium points

February 25, 2012

Suppose we are given a dynamical system of the form

$\dot{x} (t) = f ( x (t) )$

where $x : \mathbb{R} \to \mathbb{R}^n$ is the state trajectory, and $f : \mathbb{R}^n \to \mathbb{R}^n$ is a known vector field [1]. We now introduce the following definition:

Definition: A point $x^* \in \mathbb{R}^n$ is an equilibrium point of the given dynamical system if the state being at $x^*$ at some time $t^*$ implies that the state will remain at $x^*$ for all future time, i.e., $x (t) = x^*$ for all $t \geq t^*$. In other words, an equilibrium point $x^*$ is a point of zero flow, i.e., $f ( x^* ) = 0$.

If you happen to dislike the word “flow”, feel free to replace it with the word “velocity”. A point of zero velocity is thus a stationary one. Like a properly-trained poodle, it stays put.

One can find the equilibrium points of a given dynamical system by computing the real roots of the vector equation $f (x) = 0$. However, suppose that we are not interested in computing the equilibrium points; instead, all we would like to know is whether any such points exist. Thus, we arrive at the following decision problem:

Problem: Given a vector field $f : \mathbb{R}^n \to \mathbb{R}^n$, we would like to decide whether the dynamical system $\dot{x} (t) = f ( x (t) )$ has at least one equilibrium point. This is equivalent to determining the truth value of the formula $\exists x \left( f (x) = 0 \right)$, where $x \in \mathbb{R}^n$.

Since both $x$ and $f (x)$ are $n$-dimensional vectors, $x = (x_1, \dots, x_n)$ and $f (x) = (f_1 (x), \dots, f_n (x))$, we can rewrite the existentially-quantified formula above in the following form

$\displaystyle\exists x_1 \exists x_2 \dots \exists x_n \left( \bigwedge_{i=1}^n f_i (x_1, x_2, \dots, x_n) = 0\right)$.

Can one even determine the truth value of the existentially-quantified formula above? In order to avoid colliding against the brick wall of undecidability, let us restrict our attention to polynomial dynamical systems (i.e., dynamical systems in which the vector field $f : \mathbb{R}^n \to \mathbb{R}^n$ is polynomial). For such systems, one can use quantifier elimination to decide the existence of equilibrium points.

__________

Example

Consider the following polynomial dynamical system

$\begin{array}{rl} \dot{x}_1 &= \mu - x_1^2\\ \dot{x}_2 &= - x_2\end{array}$

taken from section 2.7 in Khalil’s book [1]. Note that the two first-order ordinary differential equations above are decoupled, i.e., they are of the form $\dot{x}_i = f_i (x_i)$. Note also that we have a free parameter $\mu \in \mathbb{R}$.

We now compute the equilibrium points of the dynamical system by solving the (scalar) polynomial equations $f_i (x_i) = 0$. We thus obtain $x_1^2 = \mu$ and $x_2 = 0$. For $\mu > 0$, we have two equilibrium points at $(\sqrt{\mu}, 0)$ and $(-\sqrt{\mu}, 0)$. For $\mu = 0$, we have one equilibrium point at $(0,0)$. Finally, for $\mu < 0$, we have no equilibrium points, as the equation $x_1^2 = \mu$ has no real roots when $\mu < 0$. The existence of equilibrium points depends on parameter $\mu$. Stating that this dynamical system has at least one equilibrium point is the same as saying that the following existentially-quantified formula

$\displaystyle\exists x_1 \exists x_2 \left( x_1^2 - \mu = 0 \land x_2 = 0\right)$

evaluates to $\text{True}$. By visual inspection of the formula, we conclude that the formula (which has two bound variables, $x_1$ and $x_2$, and one free variable $\mu$) evaluates to $\text{True}$ when $\mu \geq 0$. Let us confirm this using the following REDUCE + REDLOG script:

% decide the existence of equilibrium points

rlset ofsf;

% define polynomial vector field
f1 := mu - x1**2;
f2 := -x2;

% define existentially quantified formula
phi := ex({x1,x2}, f1=0 and f2=0);

% perform quantifier elimination
rlqe phi;

end;

which outputs $\mu \geq 0$. Hence, if the parameter $\mu$ is nonnegative, then there will always exist at least one equilibrium point.

__________

References

[1] Hassan K. Khalil, Nonlinear Systems, 3rd edition, Prentice Hall.