If-Then with disjunctions (OR) in Integer Linear Programming (ILP)
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.