Re: [Help-glpk] binary boolean

[Andrew Makhorin]

> Is there a default that can be applied? It seems that the boolean
> operator question keeps being asked (infrequently) , and very similar
> answers provided.
> 
> Starting with the z=x OR y example- it would be interesting to get
> several different ways of implementing that, in addition to the one
> already proposed.
> 

(All variables are assumed to be binary.)

1. Most natural description based on CNF (satisfiability)

   Let

      f(x,y,z): z = x OR y

   is a Boolean function. Then its truth table is the following:

   x  y  z  f(x,y,z)
   -----------------
   0  0  0      1
   0  0  1      0
   0  1  0      0
   0  1  1      1
   1  0  0      0
   1  0  1      1
   1  1  0      0
   1  1  1      1

   We need to exclude the points at which f takes on the value false.
   For example, f(0,0,1) = 0, so

   NOT (x = 0 AND y = 0 AND z = 1)   ==>

   x = 1 OR y = 1 OR z = 0   ==>

   x = 1 OR y = 1 OR (1 - z)    ==>

   x + y + (1 - z) >= 1   

   The complete description includes the following four inequalities:
   
        x  +      y  + (1 - z) >= 1   

        x  + (1 - y) +      z  >= 1

   (1 - x) +      y  +      z  >= 1

   (1 - x) + (1 - y) +      z  >= 1

   It is a good description, because it corresponds to the feasibility
   problem. 

2. Another description

   0 <= 2 * z - x - y <= 1

3. Yet another description (as pointed out by Erwin and Michael)

   z >= x

   z >= y

   z <= x+y

   It is a good description, because all inequalities are facet-defined
   (until the mip instance includes other constraints).

Below here are more examples:

Logical condition       Description
-----------------------------------------------------------
z = NOT x               z = 1 - x

x1 OR ... OR xn         x1 + ... + xn >= 1

x IMPL y                x <= y

z = x AND y             0 <= x + y - 2 * z <= 1

z = x1 AND ... AND xn   0 <= x1 + ... + xn - n * z <= n - 1

z = x OR y              0 <= 2 * z - x - y <= 1

z = x1 OR ... OR xn     0 <= n * z - x1 - ... - xn <= n - 1

z = x XOR y             x + y = 2 * s + z, where s is binary