-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmld_logic_vs_inequalities.qmd
201 lines (155 loc) · 7.83 KB
/
mld_logic_vs_inequalities.qmd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
---
title: "Logic vs inequalities"
bibliography:
- ref_hybrid.bib
- ref_mpc.bib
csl: ieee-control-systems.csl
format:
html:
html-math-method: katex
code-fold: true
code-summary: "Show the code"
crossref:
fig-prefix: Fig.
eq-prefix: Eq.
engine: julia
---
Our goal is to reformulate the logical conditions (such as IF-THEN-ELSE) encountered in the discrete hybrid model (DHA) as inequalities (and possibly equations), 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 reformulated as linear inequalities.
## Propositional logic and connectives
Propositions (also logical formulas) are either true or false. They are composed of elementary or atomic propositions (also 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 symbols that represent logical values.
### Connectives
- Conjunction (logical and): $X_1 \land X_2$
- Disjunction (logical or): $X_1 \lor X_2$
- Negation: $\neg X_2$
- Implication: $X_1 \rightarrow X_2$
- Equivalence: $X_1 \leftrightarrow X_2$
- Logical XOR: $X_1 \oplus X_2$
## Equivalences of logical propositions
We will heavily used the following equivalences between logical propositions:
$$
\begin{aligned}
X_1 \rightarrow X_2 \qquad &\equiv \qquad \neg X_2 \rightarrow \neg X_1,\\
X_1 \leftrightarrow X_2 \qquad &\equiv \qquad (X_1 \rightarrow X_2) \land (X_2 \rightarrow X_1),\\
X_1 \land X_2 \qquad &\equiv \qquad \neg (\neg X_1 \lor \neg X_2),\\
X_1 \rightarrow X_2 \qquad &\equiv \qquad \neg X_1 \lor X_2.
\end{aligned}
$$
The first three are certainly well known. If the last one does not look familiar, it can be seen as follows: for no $X_1$ and $X_2$ does $X1 \land \neg X2$ evaluate to true. In other words, $\neg(X1 \land \neg X2)$ is true. De Morgan then gives $\neg X1 \lor X2$.
:::{.callout-caution}
## Two kinds of equivalence
It may be confusing that we use the term *equivalence* in two different meanings here and with two different symbols. Indeed, the symbol $\leftrightarrow$ (sometimes also called material equivalence or biconditional) is a part of the logical proposition, while the symbol $\equiv$ is used to relate two logical propositions. While this is well established and described in the literature, the notation varies wildly. In particular, beware that the symbol $\iff$ can frequently be encountered in both contexts (that is why we avoid it here). On the other hand, we take the liberty to refer to both cases just as the *equivalence*, hoping that the context will make it clear which one is meant.
:::
## 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 \quad \leftrightarrow \quad [\delta = 1].$$
:::{.callout-important}
## Redudant (but convenient) use of brackets
Strictly speaking, the brackets are redundant here. We can equally well write $X \leftrightarrow \delta = 1$, assuming precedence of $=$ over $\leftrightarrow$. In this regard, the role of the brackets is really just to emphasize the precedence visually. There is also nothing special about the square brackets, we could equally well write $X \leftrightarrow (\delta = 1)$.
:::
## Integer equations and (in)equalities related to the logical formulas
Having introduced binary variables, we now aim at reformulating logical formulas into equivalent integer equalities or inequalities. Let's investigage one logical connective after another.
### And (conjunction)
We first consider the conjunction of two logical variables $X_1$ and $X_2$:
$$X_1 \land X_2.$$
Invoking binary variables, we can rewrite this as
$$[\delta_1=1] \land [\delta_2=1],$$
which ultimately translates to the system of two (trivial) equations
$$
\begin{aligned}
\delta_1&=1,\\
\delta_2&=1.
\end{aligned}
$$
Another possibility is
$$
\delta_1 + \delta_2 = 2.
$$
From the perspective of subsequent optimization for which this constitutes a constraint, hardly anything can be gained by this formulation compared to the previous one.
Yet another possibility is
$$\delta_1 \delta_2 = 1,$$
but we discard it immediately, because it is nonlinear and it provides not advantage over the previous linear formulation.
### Or (disjunction)
Another logical formula is
$$X_1 \lor X_2, $$
which with binary variables becomes
$$[\delta_1=1] \lor [\delta_2=1].$$
It can be equivalently expressed as
$$\delta_1 + \delta_2\geq 1.$$
### Negation
The negation
$$\neg X_1$$
expressed using a binary variable as in
$$\neg [\delta_1=1]$$
leads to the equation
$$\delta_1 = 0.$$
### Xor
The exclusive OR
$$X_1 \oplus X_2,$$
$$[\delta_1=1] \oplus [\delta_2=1],$$
leads to the equation
$$\delta_1 + \delta_2 = 1.$$
### Implication
We now consider the implication
$$X_1 \rightarrow X_2,$$
$$[\delta_1=1] \rightarrow [\delta_2=1].$$
We can take advantage of the equivalent formula
$$\neg X_1 \lor X_2,$$
which in terms of binary variables is
$$\neg [\delta_1=1] \lor [\delta_2=1],$$
which can be equivalently expressed as an inequality
$$(1-\delta_1) + \delta_2\geq 1,$$
which further simplifies to
$$\delta_1 - \delta_2 \leq 0.$$
### Equivalence
The equivalence
$$X_1 \leftrightarrow X_2,$$
$$[\delta_1=1] \leftrightarrow [\delta_2=1]$$
can be viewed as a conjunction of two implications, which then gives
$$\delta_1 - \delta_2 = 0.$$
### Assignment (product)
We now investigate the following logical formula
$$X_3 \leftrightarrow (X_1 \land X_2),$$
which after introducing binary variables becomes
$$[\delta_3=1] \leftrightarrow ([\delta_1=1] \land [\delta_2=1]).$$
The motivation as well as the justification of the name(s) will become clear later in this section when we discuss the interplay between logic and continuous variables (the `IF-THEN-ELSE` case).
Expressing the equivalence using implications
$$(X_3 \rightarrow X_1) \land (X_3\rightarrow X_2) \land ((X_1 \land X_2) \rightarrow X_3).$$
The last of the tree terms connected by the $\land$ connective 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 is represented with binary variables as
$$\neg [\delta_1=1] \lor \neg [\delta_2 = 1] \lor [\delta_3 = 1],$$
which finally leads to the linear inequality
$$(1-\delta_1) + (1-\delta_2) + \delta_3 \geq 1.$$
After simplification, and brinding in also the inequality formulations for the other two terms, we get
$$
\begin{aligned}
\delta_1 + \delta_2 - \delta_3 &\leq 1,\\
-\delta_1 + \delta_3 &\leq 0,\\
-\delta_2 + \delta_3 &\leq 0.
\end{aligned}
$${#eq-product-assignment}
### General transformation of Boolean expressions to integer inequalities
While logical formulas can be fairly diverse, it is often advantageous to use equivalences to reformulate them into some special forms. One particular form that we prefer here is the *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].
$$
The reason for our preference has already been displayed in @eq-product-assignment above. Namely, the logical conjunction $\land$ translates to the requirement of a simultaneous satisfaction of inequalities or equations as in
$$
\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}
$$