12 Satisfibility V (Horn Clauses) (sat5)

Run LPL Code  ,  PDF Document


Check whether x is implied by the three following (Horn) clauses:

x ∧ y →  z,  w ∧ z ∧ y →  x,  x →  y

Modeling Steps

It is a CNF (Conjunctive Normal Form) where the clauses are Horn clauses (clauses that have at most one positive literal, see sat1.

Listing 5: The Complete Model implemented in LPL [13]
model SAT5 "Satisfibility V (Horn Clauses)"; 
  binary variable x; y; z; w; 
    R1: x and y -> z; 
    R2: w and z and y -> x; 
    R3: x -> y; 
  minimize obj: x; 

If a model consists of Horn clauses then one can solve the LP relaxation of the corresponding 0-1-ILP to solve the problem, although the solution may not be necessarily have an integer solution. We can nevertheless deduce the result from the optimal value. Hence, no branching is needed.


In this model, the LP relaxation give an optimal value of zero. Hence, x does not follow from the premises. As one can easily verify, the feasible points are:

  (x,y,z,w) =

This list shows that x is not true under all interpretations.

Further Comments

This model corresponds to the following Prolog program (since all constraints are Horn clauses):

   z :- x, y        // three rules
   x :- w, z, y
   y :- x
   ?- x             // the goal to prove


  1. Translate the following Prolog program into LPL and solve it. What is the optimum of the 0-1-ILP, what is the optimum of the LP relaxation?

              x, y, z
              x :- y, z
              ?- y, z


  1. The model in LPL is as follows and gives the optimal value solution of -1

            model Horn1;
              binary variable x; y; z;
                c1: ~x or ~y or ~z;
                c2: x or ~y or ~z;
              minimize obj: ~y or ~z;

    The LP relaxation is as follows and give an optimum of -1.5:
            model Horn1;
              variable x[0..1];y[0..1];z[0..1];
              minimize obj:  -z-y;
              constraint c1: -z - y - x >= -2;
                         c2: -z - y + x >= -1;

    (The expression ~y or ~z is a separating cut.)