Let's say I want to set x1=1 if (x2=1 AND x3=1 AND x4=1) or (x5=1 and x6=1) or (x7=1) else x1=0
All of the xs are binary variables.
My first thought is I have to add 3 additional variables, let's say y1, y2, y3 and 12 constraints like this
3*y1-x2-x3-x4<=0
y1-x2>=0
y1-x3>=0
y1-x4>=0
2*y2-x5-x6<=0
y2-x5>=0
y2-x6>=0
y3-x7=0
3*x1-y1-y2-y3>=0
x1-y1<=0
x1-y2<=0
x1-y3<=0
Is there a more efficient way to tackle this?
It can be done with two auxiliary variables, y1,y2:
x1 >= y1
x1 >= y2
x1 <= y1 + y2
x2 + x3 + x4 >= 3*(y2 - y1)
x2 + x3 + x4 <= 2 + y1 + y2
x5 + x6 >= 2*(y1 - y2)
x5 + x6 <= 1 + y1 + y2
x7 >= y1 + y2 - 1
x7 <= y1 + y2
The idea here is that if (y1,y2) = (0,1), then the first and-clause is forced to be true; if (y1,y2) = (1,0), then the second and-clause is forced to be true; if (y1,y2) = (1,1), then the third and-clause is forced to be true; and if (y1,y2) = 0, then all three and-clauses are forced to be false.
In other words, (y1,y2) represents the index (in binary) of which of the three and-clauses is true; or (0,0) if none of them are true.
I would be surprised if it is possible to encode your constraint using only a single auxiliary variable.
This trick can be generalized: if you have an OR of $2^k-1$ AND-clauses, then you can find an encoding that uses $k$ auxiliary variables.
