If-Then with disjunctions (OR) in Integer Linear Programming (ILP) I have the following constraints I'm trying to model in Linear Integer Programming. I will try out diverse solvers for this later, but first I need to model the problem.

Given the integer variables: x1, x2, x3, x4, y1, y2, y3, y4, I have the following constraints:

IF (y1 ≤ y3 ≤ y2  OR  y1 ≤ y4 ≤ y2)
THEN (x1 ≥ x4  OR  x2 ≥ x3)


Additionally for all of these variables I have upper and lower bounds.

I think I have to use the "big M" technique, but I'm not sure how to handle the logical OR in the IF condition and in the THEN condition and how to built up one complete model.

Does anyone of you know how to resolve this?
Many thanks in advance.
You have the following condition:

IF ((y1 &lt;= y3) AND (y3 &lt;= y2)) OR ((y1 &lt;= y4) AND (y4 &lt;= y2))
THEN (x1 &gt;= x4) OR (x2 &gt;= x3)


For each logical term, you'll need a new binary variable. At each "level" of the logical statements, you'll use the binary variables from the previous level. So:


z1 = 1 iff y1 &lt;= y3
z2 = 1 iff y3 &lt;= y2
z3 = 1 iff z1 = 1 AND z2 = 1 
z4 = 1 iff y1 &lt;= y4
z5 = 1 iff y4 &lt;= y2
z6 = 1 iff z3 = 1 AND z4 = 1
z7 = 1 iff x1 &gt;= x4
z8 = 1 iff x2 &gt;= x3


Then you'll have a constraint that says:


if z3 = 1 OR z6 = 1 then z7 = 1 OR z8 = 1


Let's take one type of constraint at a time. 

z1 = 1 iff y1 &lt;= y3:

y3 - y1 + 1 &lt;= Mz1
y1 - y3 &lt;= M(1 - z1)


The logic is: If y3 &gt; y1 - 1, i.e., y3 &gt;= y1, then z1 must equal 1. If y1 &gt; y3 + 1, i.e., y1 &gt; y3, then z1 must equal 0.

Note that if the y variables are continuous, not integer, then replace the 1s with some small number. This isn't ideal from a numerical perspective though.

Constraints 2, 4, 5, 7, and 8 are similar.

z3 = 1 iff z1 = 1 AND z2 = 1:

z1 + z2 &lt;= 2z3
z3 &lt;= z1
z3 &lt;= z2


The logic is: If z1 and z2 both equal 1, then z3 must equal 1. If either of them equals 0, then z3 must equal 0.

Constraint 6 is similar.

if z3 = 1 OR z6 = 1 then z7 = 1 OR z8 = 1:

z3 + z6 &lt;= 2(z7 + z8)


The logic is: If z3 = 1 or z6 = 1, then z7 or z8 must equal 1.