11 Satisfibility IV (sat4)

Run LPL Code  ,  PDF Document


Check whether x2 follows from the following conjunctive normal form (CNF):

(x1 ∨ x2 ∨ x3) ∧ (x1-∨ x2 ∨ x4) ∧ (x1-∨ x3) ∧ (x1-∨ x3-∨ x4) ∧ (x1 ∨ x3)

Modeling Steps

  1. Each of the five clauses can be formulated as a constraint, since a list of constraints is the same as a conjunction of constraints.

  2. Minimize the expression x2 subject to the five clauses is all we need to do. Why? Suppose minimizing x2 result in x2 = 1. This means that it is impossible to set x2 = 0. We conclude that if the five clauses are true then x2 must also be true. Suppose conversely, that the minimizing gives x2 = 0. This means that x2 does not follow from the five clauses, since the five constraints are true and x2 is false. Hence x2 does not follow from the constraints.

  3. We conclude that the objective function expression follows from the constraints if and only if its value is greater or equal one (1).

Listing 4: The Complete Model implemented in LPL [13]
model SAT4 "Satisfibility IV"; 
  binary variable x1; x2; x3; x4; 
    R1: x1 or x2 or x3; 
    R2: ~x1 or x2 or ~x4; 
    R3: ~x1 or x3; 
    R4: ~x1 or ~x3  or x4; 
    R5: x1 or ~x3; 
  minimize obj: x2; 


Since the optimal value for this model is x2 = 1, we conclude that x2 follows from the five clauses.

Further Comments

LPL translates this Boolean model into a pure 0-1 linear program as follows:

  model SAT4;
    binary variable x1; x2; x3; x4;
      R1: x1+x2+x3  >= 1;
      R2: -x1+x2-x4 >= 1-2;
      R3: -x1+x3    >= 1-1;
      R4: -x1-x3+x4 >= 1-2;
      R5: x1-x3     >= 1-1;
    minimize obj: x2;