Logic vs mixed integer-linear inequalities

Our goal is to turn the IF-THEN-ELSE conditions in the discrete hybrid model (DHA) into linear inequalities, which will allow us to formulate the model as a mathematical program, actually a mixed-integer program (MIP). In order to get there, we are going to recap some fundamentals of logic and then we are going to show how various logical conditions can be turned into linear inequalities.

Propositional logic and connectives

Propositions that are either true or false are composed of elementary propositions (Boolean variables) and connectives.

Boolean variable (or elementary proposition)

X evaluates to true or false. Oftentimes values 0 and 1 are used, but it should be clear that these are not numbers but logical values.

Connectives

• Conjunction (logical and): X_1 \land X_2
• Disjunction (logical or): X_1 \lor X_2
• Negation: \neg X_2 (or \overline{X_2} or \sim X_2)
• Implication: X_1 \implies X_2
• Equivalence: X_1 \iff X_2
• Logical XOR: X_1 \oplus X_2

Equivalences of logic propositions

We will heavily used the following equivalences: \begin{aligned} X_1 \implies X_2 \qquad &\equiv \qquad \neg X_2 \implies \neg X_1,\\ X_1 \iff X_2 \qquad &\equiv \qquad (X_1 \implies X_2) \land (X_2 \implies X_1),\\ X_1 \land X_2 \qquad &\equiv \qquad \neg (\neg X_1 \lor \neg X_2),\\ X_1 \implies X_2 \qquad &\equiv \qquad \neg X_1 \lor X_2. \end{aligned}

The last one can be seen as follows: it cannot happen that X1 \land \neg X2, that is, it holds that \neg(X1 \land \neg X2). De Morgan gives \neg X1 \lor X2.

Binary variables related to the Boolean ones

Ultimately we want to use numerical solvers to solve optimization problems. In order to do that, we need to associate with the Boolean variable X a binary (integer) variable \delta\in\{0,1\} such that \delta = \begin{cases} 0 & \text{if} \; \neg X,\\ 1 & \text{if} \; X. \end{cases}

In other words, have the the following equivalence X \qquad \iff \qquad [\delta = 1].

Redudant (but convenient) use of brackets

The use of the brackets here is redundant. As long as the symbol = is interpreted as equation and not assignment, we can equally well write X \equiv \delta = 1, assuming precedence of = over \iff. In this regard, the role of the brackets is really just grouping. We could also use X \equiv (\delta = 1) for that matter.

Integer (in)equalities related to the logical formulas

Having introduced binary variables, we now aim at reformulating logical formulas into equivalent integer equalities or inequalities.

And (conjunction)

We first consider the conjunction of two logical variables X_1 and X_2: X_1 \land X_2.

Invoking the binary variables, we can rewrite this as [\delta_1=1] \land [\delta_2=1], which ultimately translates to \delta_1=1, \; \delta_2=1.

Another possibility is \delta_1 \delta_2 = 1, but we discard it because it is nonlinear and we prefer the linear version for obvious reasons.

Or (disjunction)

X_1 \lor X_2

[\delta_1=1] \lor [\delta_2=1]

\delta_1 + \delta_2\geq 1

Negation

\neg X_1

\neg [\delta_1=1]

\delta_1 = 0

Xor

X_1 \oplus X_2

[\delta_1=1] \oplus [\delta_2=1]

\delta_1 + \delta_2 = 1

Implication

X_1 \implies X_2

[\delta_1=1] \implies [\delta_2=1]

Equivalently, using \neg X_1 \lor X_2 we get \neg [\delta_1=1] \lor [\delta_2=1], which translates to (1-\delta_1) + \delta_2\geq 1, which simplifies to \delta_1 - \delta_2 \leq 0.

Equivalence

X_1 \iff X_2 [\delta_1=1] \iff [\delta_2=1]

\delta_1 - \delta_2 = 0

Assignment

X_3 \iff (X_1 \land X_2)

[\delta_3=1] \iff ([\delta_1=1] \land [\delta_2=1])

Expressing the equivalence using implications X_3 \implies X_1,\; X_3\implies X_2, \; (X_1 \land X_2) \implies X_3

The the last one is equivalent to \neg (X_1 \land X_2) \lor X_3, which can be simplified to \neg X_1 \lor \neg X_2 \lor X_3, which translates to \neg [\delta_1=1] \lor \neg [\delta_2 = 1] \lor [\delta_3 = 1], which finally leads to the inequality (1-\delta_1) + (1-\delta_2) + \delta_3 \geq 1 and after simplification \delta_1 + \delta_2 - \delta_3 \leq 1.

And don’t forget to consider the first two inequalities too -\delta_1 + \delta_3 \leq 0, \quad -\delta_2 + \delta_3 \leq 0.

General transformation of Boolean expressions to integer inequalities

From Conjunctive Normal Form (CNF) \bigwedge_{j=1}^m \left[\left(\lor_{i\in \mathcal{P}_j} X_i\right) \lor \left(\lor_{i\in \mathcal{N}_j} \neg X_i\right)\right] to 0-1 integer inequalities defining a polyhedron \begin{aligned} \sum_{i\in \mathcal{P}_1} \delta_i + \sum_{i\in \mathcal{N}_1} (1-\delta_i) &\geq 1,\\ &\vdots\\ \sum_{i\in \mathcal{P}_m} \delta_i + \sum_{i\in \mathcal{N}_m} (1-\delta_i) &\geq 1. \end{aligned}

Finite state machine (FSM) using binary variables

For characterization of discrete states (both in discrete-event and hybrid systems), we used integer variables. But now, with anticipation of using numerical solvers, we will use binary variables. We encode the discrete state variable x_d in binary. As a matter of fact, vector variables are needed here x_b \in \{0,1\}^{n_b}.

Similarly the discrete inputs u_b \in \{0,1\}^{m_b}.

The logical state equation then x_b(k+1) = f_b(x_b(k),u_b(k),\delta_e(k)).

Example 1 (Example)  

Figure 1: Example of a FSM

The state update/transition equation is \begin{aligned} x_d(k+1) = \begin{cases} \text{Red} & \text{if}\; ([x_d = \text{green}] \land \neg [\delta_3=1]) \lor ([x_d = \text{red}] \land \neg [\delta_3=1])\\ \text{Green} & \text{if} \; \ldots\\ \text{Blue} & \text{if} \; \ldots \end{cases} \end{aligned}

Binary encoding of the discrete states \text{Red}: x_b = \begin{bmatrix}0\\0 \end{bmatrix}, \; \text{Green}: x_b = \begin{bmatrix}0\\1 \end{bmatrix}, \; \text{Blue}: x_b = \begin{bmatrix}1\\0 \end{bmatrix}

Reformulating the state update equations for binary variables \begin{aligned} x_{b1} &= (\neg [x_{b1} = 1] \land \neg [x_{b2} = 1] \land [\delta_1=1] \land \neg[u_{b2}=1]) \\ &\quad \lor (\neg [x_{b1} = 1] \land [x_{b2} = 1] \land [\delta_3=1] \land [u_{b1}=1])\\ &\quad \lor ([x_{b1} = 1]\land [x_{b2} = 1] \land \neg [\delta_2=1])\\ x_{b2} &= \ldots \end{aligned}

Finally, simplify, convert to CNF.

Mixing logical and continuous through indicator variables

Now that we have learnt to encode purely logical expressions into inequalities, we consider the cases where logical and continuous variables are mixed. We aim at the same kind of encoding as before, that is, we want to formulate inequalities.

Logical implies continuous

We start by considering the implication X \implies [f(x)\leq 0], where X is a Boolean variable and f(x) is a real-valued function of a real variable x. Upon represented the Boolean variable X with the binary variable \delta (called an indicator variable) we can write the implication as [\delta = 1] \implies [f(x)\leq 0].

In order to construct an equivalent inequality, we introduce a real parameter M large enough such that when \delta=0 in f(x) \leq (1-\delta) M, there is no practical restriction on f. If \delta=1, the original inequality is trivially enforced.

Big-M technique

This is a popular trick and is known as the Big-M technique. It is not a trouble-free trick, though. It is important to avoid setting M unnecessarily too high. See the section Dealing with Big-M Constraints in Gurobi Reference Manual for some discussion of numerical issues.

Continuous implies logical

The other implication [f(x)\leq 0] \implies X, with the Boolean variable X represented with a binary \delta as [f(x)\leq 0] \implies [\delta = 1], can be written equivalently as \neg [\delta = 1] \implies \neg [f(x)\leq 0], which can be further simplified to [\delta = 0] \implies [f(x) > 0].

We now introduce m small enough such that that f(x) is practically unrestricted when \delta=1 in f(x) > m\delta, while f(x)>0 is trivially enforced when \delta=0.

For numerical reasons, we modify the strict equality to nonstrict inequality f(x) \geq \epsilon + (m-\epsilon)\delta, where \epsilon\approx 0 (for example, machine epsilon).

Equivalence between logical and continuous

Now we combine the previous two implications so that we can write the equivalence X \iff [f(x)\leq 0],

represented through the indicator variable \delta as \boxed{ [\delta = 1] \iff [f(x)\leq 0], }

as the two inequalities \boxed{ \begin{aligned} f(x) &\leq (1-\delta) M,\\ f(x) &\geq \epsilon + (m-\epsilon)\delta. \end{aligned}} \tag{1}

IF-THEN-ELSE rule as an inequality

We now consider the following IF-THEN-ELSE rule:

\mathrm{if} \; X, \; \mathrm{then} \; z = f(x,u), \; \text{else} \; z = 0.

It can be equivalently expressed as the product z = \delta\,f(x,u), where \delta is a binary indicator. This, in turn, can be written as \begin{aligned} z &\leq M\delta,\\ - z &\leq -m\delta,\\ z &\leq f(x,u) - m(1-\delta),\\ -z &\leq -f(x,u) + M(1-\delta). \end{aligned}

Scalar functions only

Beware that the above results are valid only for scalar functions f(), even if their arguments are possibly vectors.

Particularly useful from a computational viewpoint will be an affine function f(x,y) = ax + bu + e. We specialize the above inequalities to this case for later convenience. \boxed{ \begin{aligned} z &\leq M\delta,\\ - z &\leq -m\delta,\\ z &\leq ax + bu + e - m(1-\delta),\\ -z &\leq -(ax + bu + e) + M(1-\delta). \end{aligned}} \tag{2}

Another IF-THEN-ELSE rule

Another IF-THEN-ELSE rule (and here we already specialized it to affine functions) can also be useful:

\mathrm{if} \; X, \; \mathrm{then} \; z = a_1x + b_1u + e_1, \; \mathrm{else} \; z = a_2x + b_2u + e_2.

Using a binary indicator \delta, it can be expressed as z = {\color{blue}\delta}\,(a_1 x + b_1 u + e_1) + {\color{blue}(1-\delta)}(a_2 x + b_2 u + e_2), which can be rewritten as \boxed{ \begin{aligned} (m_2-M_1)\delta + z &\leq a_2 x + b_2 u + e_2,\\ (m_1-M_2)\delta - z &\leq -a_2 x - b_2 u - e_2,\\ (m_1-M_2)(1-\delta) + z &\leq a_1 x + b_1 u + e_1,\\ (m_2-M_1)(1-\delta) - z &\leq -a_1 x - b_1 u - e_1. \end{aligned}} \tag{3}

Generation of events by mixing logical and continuous variables in inequalities

Application of Equation 1 to the ith event generator function h_i(x,u) leads to the following inequalities \boxed{ \begin{aligned} h_i(x_c(k), u_c(k)) &\leq M_i (1-\delta_{e,i}),\\ h_i(x_c(k), u_c(k)) &\geq \epsilon + (m_i-\epsilon) \delta_{e,i}. \end{aligned}} \tag{4}

Switched affine system

We are now ready to get rid of the IF-THEN(-ELSE) conditions in the definition of the switched affine system by reformulating it as inequalities. Namely, we consider x_c(k+1) = \sum_{i=1}^s z_i(k), where z_1(k) = \begin{cases} a_1 x_c(k) + b_1 u_c(k) + f_1 & \text{if}\;i(k)=1,\\ 0 & \text{otherwise}, \end{cases} \quad \vdots z_s(k) = \begin{cases} a_s x_c(k) + b_s u_c(k) + f_s & \text{if}\;i(k)=s,\\ 0 & \text{otherwise}, \end{cases} and we rewrite it for each i\in \{1, 2, \ldots, s\} as \boxed{ \begin{aligned} z_i &\leq M_i\delta_i,\\ - z_i &\leq -m_i\delta_i,\\ z_i &\leq a_i x + b_i u + f_i - m_i(1-\delta_i),\\ -z_i &\leq -(a_i x + b_i u + f_i) + M_i(1-\delta_i). \end{aligned}} \tag{5}

All these results were derived just for scalar z and f()

With the formalism presented here, vector variables \bm z and correspondingly vector right-hand-side functions \mathbf f() must be handled but considering their individual scalar components z_1, \ldots, z_n and f_1(), \ldots, f_n(). Notational care must be exercised, note that the lower index in this remark has different meaning than that in Equation 5.