Logic vs inequalities

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.

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].

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} \tag{1}

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. 1 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}