generalized_cnf.tex

由matlab开发的hybrid系统的描述语言

\chapter{More on Generalized Conjunctive Normal Form} \label{app:A}
%In this section we propose an algorithm for the systematic
%translation of complex logical propositions into mixed-integer
%inequalities. We
In the sequel, we assume that upper and lower bounds are known on
real affine functions $f_i(x)=a_i'x-b_i$, $f_i:\rr^n\mapsto\rr$.
Consider the logic disjunction $
    \bigvee_{i=1}^{m} [f_i(x) \leq 0]
    \label{eq.orfi}
$ which in general defines a nonconvex set in $\rr^n$, e.g. the
set of Figure \ref{fig.ory1y2}, corresponding to the disjunction
$%\begin{equation}
    \left[ x_1\leq 0 \right] \vee \left[ x_2 \leq 0 \right] \label{eq.ory1y2}
$, %\end{equation}
where $m_1\leq x_1\leq M_1$, $m_2\leq x_2\leq M_2$.
\figuraeps{elle}{t}{4cm}{Feasible set defined by
(\ref{eq.ory1y2})}{fig.ory1y2} Although the set in Figure
\ref{fig.ory1y2} is nonconvex, by introducing an additional binary
variable $\delta\in\{0,1\}$ and then relaxing the integrality
constraints to $0\leq\delta\leq 1$, the set can be represented as
a convex polyhedral set in the higher dimensional space $\rr^3$,
i.e., as a set of linear inequalities. Here we provide a general
procedure for translating disjunctions of linear-threshold
conditions into a set of mixed-integer linear inequalities.

\begin{theorem}
\label{th.orcont} The logical proposition with $m$ affine
functions $f_{i}(x)$
\begin{equation}
    \bigvee_{i=1}^{m} [f_{i}(x) \leq 0]
    \label{eq.bigvee}
\end{equation}
can be translated into a set of mixed integer inequalities by
adding  $\ell = \lceil \log_2(m') \rceil$ binary variables, where
$m' \leq m$ is the number of non-redundant constraints
\end{theorem}

%A constraint $[f_j(x) \leq 0]$ is {\em redundant} for the proposition (\ref{eq.bigvee}), if
%\[
%\left\{ x: \bigvee_{i=1}^{m} [f_{i}(x) \leq 0] \right\} = \left\{ x:
%     \bigvee_{i=1, i\neq j}^{m} [f_{i}(x) \leq 0] \right\}
%\]

\begin{proof}
The proof is constructive and involves the following steps
\begin{enumerate}
\item Define the closure of the infeasible set $B$ as
\footnote{Note that we include the edge points in $B$.} $ B = \{x:
\bigwedge_{i=1}^m [f_i(x) \geq 0] \} $. Since all $f_i$ are
affine, $B$ is convex.
\item \label{step.redrem} Eliminate the redundant constraints.
     This can be done by solving $m$ linear programs of the form
\begin{equation}
    \ba{ll}
    \max_{x} &f_i(x)\\
    \mbox{s.t.} & \bigwedge_{j=1,\ j\neq i}^m[f_j(x)\leq
    0]\mbox{.}
    \ea
\end{equation}
This gives the number of non-redundant constraints $m'$. Note that
the disjunction (\ref{eq.bigvee}) can be written equivalently only
using the non-redundant constraints. This step aims at having a
minimal representation of (\ref{eq.bigvee}). Note also that $m'$
is the number of facets of the polyhedron $B$.
\item According to \cite[Theorem 3]{BMDP99},
the set $X \backslash B$ can be partitioned into $m'$ disjoint
convex sets $C_j$. Each set can be described by the inequalities
\[
C_j = \{x: A_j x \leq b_j\}
\]
where by appropriate numbering, we have $A_j \in \mathbb{R}^{j
\times s}$ and $b_j \in \mathbb{R}^j$.
\item Temporarily introduce $m'$ binary variables $\delta_j$ with the property that
\[
[\delta_j = 1] \leftrightarrow [x\in C_j] \mbox{.}
\]
According to \cite{BeMo99a}, the latter relations can be
translated into mixed integer inequalities as:
\begin{eqnarray}
A_j x - b_j             & \leq & M_j(1-\delta_j) ~~~~ (j=1\dots m') \label{eq.deltaineq}\\
\sum_{i=1}^{m'}\delta_i & =    & 1 \label{eq.sumeq1} \mbox{.}
\end{eqnarray}
\item Introduce $\ell = \lceil \log_2(m') \rceil$ binary variables $\mu_1 \ldots \mu_{\ell}$, such that
\begin{equation}
[\delta_j = 1] \leftrightarrow [j=\sum_{i=0}^{\ell-1} 2^i
\mu_{i+1}] \mbox{.}
\end{equation}
Use them in (\ref{eq.deltaineq}) to obtain:
\begin{eqnarray*}
A_1 x - b_1       & \leq & M_1   (\ell-(1-\mu_1)- \ldots - (1-\mu_{\ell})) \\
A_2 x - b_2       & \leq & M_2   (\ell-   \mu_1 - \ldots - (1-\mu_{\ell})) \\
\vdots            &      & \vdots \\
A_{m'} x - b_{m'} & \leq & M_{m'}(\ell-   \mu_1 - \ldots -
\mu_{\ell})
\end{eqnarray*}
If $m'<2^{\ell}$, add constraints to exclude the unallowed
combinations of $(\mu_1 \dots \mu_{\ell})$. For the representation
with $\delta_j$, (\ref{eq.sumeq1}) expressed the fact that exactly
one $\delta_j$ is one for each data point $x$. This is not
required anymore when working with $(\mu_1 \dots \mu_{\ell})$.
\end{enumerate}
\cvd
\end{proof}

The number of inequalities resulting from the algorithm described
above is given by (i) the bounds on either $x$ or each function
$f_i(x)$, (ii) $\sum_{i=1}^{m'} i = \frac{m'(m'+1)}{2}$
constraints defining $\mu_1, \dots, \mu_{\ell}$, and (iii) the
constraints excluding the unused combinations of $\mu_1, \dots,
\mu_{\ell}$. Note also that neglecting the redundancy removal
procedure in step \ref{step.redrem} increases the number of binary
auxiliary variables to $\lceil \log_2(m) \rceil$, but does not
change the algorithm itself.

\begin{corollary}
\label{coro.fidi} The logical proposition with $m$ affine
functions $f_{i}(x)$
\begin{equation}
\bigvee_{i=1}^{m} [f_{i}(x) \leq 0] \bigvee_{k=1}^{n} [\delta_{k}
= 1] \label{eq.orfid1}
\end{equation}
can be translated into a set of mixed integer inequalities adding
$\ell' = \lceil \log_2(m'+1) \rceil$ binary variables, where $m'
\leq m$ is the number of non-redundant constraints in the
disjunction $\bigvee_{i=1}^{m} [f_{i}(x) \leq 0]$.
\end{corollary}

\begin{proof}
Using the constructive arguments of Theorem \ref{th.orcont}, we
can model the terms involving $f_i$. Contrary to Theorem
\ref{th.orcont}, we have to assign also a combination of $(\mu_1'
\dots \mu_{\ell}')$ to the infeasible set $B$. For computational
simplicity we assign the code $[0, \dots, 0]$ to $B$. Therefore
the number of regions to code with $(\mu_1' \dots \mu_{\ell}')$ is
increased by one. The disjunction (\ref{eq.orfid1}) can then be
imposed by the inequality
\begin{equation}
\sum_{i=1}^{\ell'} \mu_i + \sum_{k=1}^{m} \delta_k \geq 1
\end{equation}
\cvd
\end{proof}


\paragraph{Proof of Theorem~\ref{th:}.}
% \begin{theorem}
% \label{th:} The logical proposition with affine functions
% $f_{ij}(x)$
% \begin{equation}
%     \bigwedge_{j=1}^{p} \left( \bigvee_{i=1}^{m_j} [f_{ij}(x) \leq 0]
%     \bigvee_{k=1}^{n_j} [\delta_{kj} = 1] \right) \label{eq.gencnf}
% \end{equation}
% can be translated into a set of mixed integer inequalities adding
% $ \sum_{j=1}^p \lceil \log_2(m'_j+1) \rceil$ binary variables,
% where $m'_j \leq m_j$ is the number of non-redundant constraints in
% the $j$-th disjunction $\bigvee_{i=1}^{m_j} [f_{ij}(x) \leq 0]$.
% \end{theorem}

%\begin{proof}
Using Corollary \ref{coro.fidi}, each term in the conjunction
(\ref{eq.gencnf}) can be translated into inequalities. The overall
conjunction can then be modeled by contemporarily imposing all
constraints obtained. \cvd
%\end{proof}
\medskip

Finally, the last step consists of translating complex expressions
involving arbitrary logic operators (like $\OR$, $\ANd$, $\NOT$,
$\rightarrow$, $\leftrightarrow$, etc.), inequalities over
continuous variables, and logic variables.
% We propose the
% following procedure to treat such expressions:
This can be done by simply considering the inequalities as
symbolic boolean variables and manipulating the overall function
according to Section \ref{sec.purelylogic}.
% \begin{enumerate}
% \item Replace each inequality over continuous variables with a
% Boolean variable $y_i$.
% \item Find the conjunctive normal form of
% the expression using the methods described in Section
% \ref{sec.purelylogic}.
% \item Replace back the Boolean variables
% $y_i$ with the conditions over continuous variables.
% \item Apply
% the theorem above
% \end{enumerate}

Note that the effectiveness of the approach presented here can be
increased, if the scheme is given the possibility to recognize
common parts in the logic relations, like the multiple occurrence
of an inequality $[f_{i0}(x) \leq 0]$ in (\ref{eq.gencnf}).