How to using linear programming to solve the logical constraints

Question

I wish to use linear programming to solve the below describe in logic. In the below example, n1, n2, n3, b1, b2, b3 are boolean variables.

The objective is to minimize c1.

Below are the constraints:

constraint 1: (（n1==n2 xor n3） && c1==2 && b1 ) || ( (n1== n2 or n3) && c1==1 && b2 ) || (( n1 == n2 and n3) 1&& c1==3 && b3)

constraint 2: n1 && n2== not n3

constraint 3: only one of b1, b2, b3 is true

May I know is it possible to encode those logical constraints into integer constraints required by linear programming tools like Gurobi or lpsolve? Or is there any tools that can make use of boolean constraints?

Thanks.

Answer 1

Your problem seems to have a very limited structure, so a solution should be much easier. Clearly c1 must be 1, 2, or 3.

1. If ( (n1== n2 or n3) && b2 ) has a solution then c1 = 1.
2. Otherwise, if n1==n2 xor n3） && b1 ) has a solution then c1 = 2.
3. Otherwise, if (( n1 == n2 and n3) && b3) has a solution then c1 = 3. (There's a typo here in the original question with a spurious 1).
4. Otherwise, there is no solution.

Constraint 3 is easy, since each of b1, b2 and b3 is used only once:

1. If (n1== n2 or n3) has a solution then c1 = 1, b2 = 1, b1 = b3 = 0.
2. Otherwise, if （n1 == n2 xor n3) has a solution then c1 = 2, b1 = 1, b2 = b3 = 0.
3. Otherwise, if (n1 == n2 and n3) has a solution then c1 = 3, b3 = 1, b1 = b2 = 0.
4. Otherwise, there is no solution.

Constraint 2 means that n3 can be calculated from n1 and n2: n3 = not (n1 and n2), so all you need to do is to try four combinations of n1 and n2, calculate n3 for each combination, and check those conditions. No linear programming or integer programming needed.

Answer 2

It is possible with mixed integer programming (not linear programming) but messy. Lets start with the easy ones:

Constraint 2:

n1 + n2 = 1 - n3

Constraint 3:

b1 + b2 + b3 = 1  (if at most one of them is true then change = to <=)

Constraint 1:

Convention: I use y to denote boolean variables and z to denote continuous non-negative variables. I also assume that there is no difference between && and AND and between || and OR.

The trick is to break it down into pieces and define each piece as a separate variable..

y1 := n1==n2 --> (（y1 xor n3） && c1==2 && b1 ) || ( (y1 or n3) && c1==1 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

y1 >= 1 - (n1 + n2)
y1 >= (n1 + n2) - 1
y1 <= 2 - 2n1 +  n2
y1 <= 2 - 2n2 + n1

---

y2 := y1 xor n3 --> (y2 && c1==2 && b1 ) || ( (y1 or n3) && c1==1 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

y2 <= y1 + x3
y2 >= y1 - x3
y2 >= x3 - y1
y2 <= 2 - y1 - x3

---

y5 := c1==2 --> (y2 && y5 && b1 ) || ( (y1 or n3) && c1==1 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

Letting epsilon > 0 be a predefined tolerance (so that if 2 - epsilon <= c1 <= 2 + epsilon then c1=2) and M a big number (possible the upper bound of c1):

z3 >= c1 - 2 + epsilon*y3;  z3 >= 0
z4 >= 2 - c1 + epsilon*y4;  z4 >= 0
z3 <= My3
z4 <= My4
y3 + y4 + y5 = 1

---

y6 := y2 && y5 && b1 --> y6 || ( (y1 or n3) && c1==1 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

y6 <= y2
y6 <= y5
y6 <= b1
y6 >= y2 + y5 + b1 - 2

---

y7 := y1 or n3 --> y6 || ( y7 && c1==1 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

y7 >= y1
y7 >= n3
y7 <= y1 + n3

---

y10 := c1 == 1 --> y6 || ( y7 && y10 && b2 ) || (( y1 and n3) 1&& c1==3 && b3)

z8 >= c1 - 1 + epsilon*y8;  z8 >= 0
z9 >= 1 - c1 + epsilon*y9;  z9 >= 0
z8 <= My8
z9 <= My9
y8 + y9 + y10 = 1

---

y11 := y7 && y10 && b2 --> y6 || y11 || (( y1 and n3) 1&& c1==3 && b3)

y11 <= y7
y11 <= y10
y11 <= b2
y11 >= y7 + y10 + b2 - 2

---

Assuming the 1&& is a typo and it is actually &&,

y12 := ( y1 and n3) --> y6 || y11 || (y12 && c1==3 && b3)

y12 <= y1
y12 <= n3
y12 >= y1 + n3 - 1

---

y15 := c1==3 --> y6 || y11 || (y12 && y15 && b3)

z13 >= c1 - 3 + epsilon*y13;  z13 >= 0
z14 >= 3 - c1 + epsilon*y14;  z14 >= 0
z13 <= My13
z14 <= My14
y13 + y14 + y15 = 1

---

y16 := y12 && y15 && b3 --> y6 || y11 || y16

y16 <= y12
y16 <= y15
y16 <= b3
y16 >= y12 + y15 + b3 - 2

---

Finally, y6 || y11 || y16

y6 + y11 + y16 >= 1

I hope this helps. For convenience, I include the full mathematical model below.

Mathematical Model

      min c1 
s.t.  n1 + n2 = 1 - n3
      b1 + b2 + b3 = 1
      y1 >= 1 - (n1 + n2)
      y1 >= (n1 + n2) - 1
      y1 <= 2 - 2n1 +  n2
      y1 <= 2 - 2n2 + n1
      y2 <= y1 + x3
      y2 >= y1 - x3
      y2 >= x3 - y1
      y2 <= 2 - y1 - x3
      z3 >= c1 - 2 + epsilon*y3;  z3 >= 0
      z4 >= 2 - c1 + epsilon*y4;  z4 >= 0
      z3 <= My3
      z4 <= My4
      y3 + y4 + y5 = 1
      y6 <= y2
      y6 <= y5
      y6 <= b1
      y6 >= y2 + y5 + b1 - 2
      y7 >= y1
      y7 >= n3
      y7 <= y1 + n3
      z8 >= c1 - 1 + epsilon*y8;  z8 >= 0
      z9 >= 1 - c1 + epsilon*y9;  z9 >= 0
      z8 <= My8
      z9 <= My9
      y8 + y9 + y10 = 1
      y11 <= y7
      y11 <= y10
      y11 <= b2
      y11 >= y7 + y10 + b2 - 2
      y12 <= y1
      y12 <= n3
      y12 >= y1 + n3 - 1
      z13 >= c1 - 3 + epsilon*y13;  z13 >= 0
      z14 >= 3 - c1 + epsilon*y14;  z14 >= 0
      z13 <= My13
      z14 <= My14
      y13 + y14 + y15 = 1
      y16 >= y12
      y16 >= y15
      y16 >= b3
      y16 >= y12 + y15 + b3 - 2
      y6 + y11 + y16 >= 1
      y1, ..., y16, b1, b2, b3, n1, n2, n3 binary
      z3, z4, z8, z9, z13, z14 >= 0

By the way, if you have accessible both lpsolve and Gurobi definitely pick Gurobi. It is the market leader, and lpsolve's performance is far off from most problems of some complexity..

UPDATE

After putting this model to a solver I get the solution c1 = 1 and

n1 = 1
n2 = 1
n3 = 1
b1 = 0
b2 = 1
b3 = 0

Which makes sense: c1 == 1 or c2 == 2 or c3 == 3 for the clause 3 to hold true, and the case c1=1 is the minimum possible. Plugging in the values for the other variables we can see that all three constraints are satisfied.

Answer 3

I think you could solve it by expressing it in constraint programming systems such as GECODE or Choco. Check them out - there are many examples to get you started.