Problem
Check whether x_{2} follows from the following conjunctive normal form (CNF):
Modeling Steps
Each of the five clauses can be formulated as a constraint, since a list of constraints is the same as a conjunction of constraints.
Minimize the expression x_{2} subject to the five clauses is all we need to do. Why? Suppose minimizing x_{2} result in x_{2} = 1. This means that it is impossible to set x_{2} = 0. We conclude that if the five clauses are true then x_{2} must also be true. Suppose conversely, that the minimizing gives x_{2} = 0. This means that x_{2} does not follow from the five clauses, since the five constraints are true and x_{2} is false. Hence x_{2} does not follow from the constraints.
We conclude that the objective function expression follows from the constraints if and only if its value is greater or equal one (1).
model SAT4 "Satisfibility IV";
binary variable x1; x2; x3; x4;
constraint
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;
Writep(x1,x2,x3,x4);
end
Solution
Since the optimal value for this model is x_{2} = 1, we conclude that x_{2} 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; constraint 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; end