Expressing an implication as ILP where each implication term comprises a chain of boolean ORs

Question

Consider an implication of the form $A \implies B$ where both $A, B$ comprises a chain of Boolean OR variables. For example, $(a_1 \lor a_2 \lor a_3) \implies (b_1 \lor b_2 \lor b_3)$. How can this be expressed as an ILP? All variables are Boolean.

I have derived the following using CNF, however it turns out to be non-linear, can this be expressed in Linear Form?

Let us suppose $A = \{ a_1, a_2, a_3\}$ and $B = \{ b_1, b_2, b_3\}$. thus,

\begin{equation} \bigvee A \implies \bigvee B \\ \overline{\bigvee A} \bigvee \left(\bigvee B\right) \\ \left(\bigwedge_{a \in A} \overline a\right) \bigvee \left(\bigvee B\right) \\ \left(\bigwedge_{a \in A} (1-a)\right) \bigvee \left(\bigvee B\right) \\ \left(\prod_{a \in A} (1-a)\right) \bigvee \left(\sum_{b \in B} b\right) \\ \prod_{a \in A} (1-a) + \sum_{b \in B} b \geq 1 \end{equation}

Thus, thus leads to $(1-a_1)(1-a_2)(1-a_3) + b_1 + b_2 + b_3 \geq 1$, which essentially leads to a product of complements of the variables in $A$. Can this be expressed in terms of linear constraints?

Answer 1

For boolean formulas, you can use the following systematic approach. First, convert your formula to conjunctive normal form. Wikipedia details how to do this.

Applied to this specific case it follows that $$(a_1 \vee a_2 \vee a_3) \Longrightarrow (b_1 \vee b_2 \vee b_3)$$ is equivalent to $$(\bar{a}_1 \vee b_1 \vee b_2 \vee b_3) \wedge (\bar{a}_2 \vee b_1 \vee b_2 \vee b_3) \wedge (\bar{a}_3 \vee b_1 \vee b_2 \vee b_3).$$

We then add a constraint for each clause: $$\begin{align} 1 - a_1 + b_1 + b_2 + b_3 & \ge 1\\ 1 - a_2 + b_1 + b_2 + b_3 & \ge 1\\ 1 - a_3 + b_1 + b_2 + b_3 & \ge 1, \end{align}$$ or equivalently $$\begin{align} a_1 &\le b_1 + b_2 + b_3\\ a_2 &\le b_1 + b_2 + b_3\\ a_3 &\le b_1 + b_2 + b_3. \end{align}$$

Note that this formulation is at least as strong as the one proposed by YukiJ, as adding the constraints together gives $$a_1 + a_2 + a_3 \le 3(b_1 + b_2 + b_3).$$

In general, different approaches may give different formulations, and I am not claiming that this is the best approach. For more information, you may consider the book Logic and Integer Programming by H. Paul Williams.

Answer 2

If I understand your question correctly then you want to model that if $$a_1+a_2+a_3\geq 1$$ then it follows that $$b_1+b_2+b_3\geq 1.$$ Since $A \implies B$ is equivalent to $\neg A \lor B$ we want to model $$\sum_{i=1}^3 a_i < 1 \quad\bigvee\quad \sum_{i=1}^3 b_i \geq 1.$$ We can replace $\sum_{i=1}^3 a_i < 1$ with $\sum\limits_{i=1}^3 a_i =0$ because the $a_i$ are binary and obtain $$\sum\limits_{i=1}^3 a_i = 0\quad\bigvee\quad\sum_{i=1}^3 b_i \geq 1.$$ This can be written as a single constraint in the following way:

$$3\sum_{i=1}^3 b_i \geq \sum_{i=1}^3 a_i $$

Now, if any of the $a_i$ is true then the constraint forces at least of of the $b_i$ to be true as well. On the other hand, if all the $a_i$ are $0$ anything can happen to the $b_i$.