Problem
Is the following set of statements logically consistent? “If the bond market goes up or if interest rates decrease, either the stock market goes down or taxes are not raised. The stock market goes down when and only when the bond market goes up and taxes are raised. If interest rates decrease, then the stock market does not go down and the bond market does not go up. Either taxes are raised or the stock market goes down and interest rates decrease.” (see [5]).
Modeling Steps
We introduce four Boolean propositions:
p "the bond market goes up" q "interest rates decrease" r "the stock market goes down" s "taxes are not raised"
Then the first statement can be formulated as: (p ∨ q) → (r ∨ s).
The second then is: r ↔ (p ∧s).
The third is: q → (r ∧p).
The final statement (the consequence) is: s ∨ (r ∧ q)
Hence we need to prove the following statement:
We minimize the last statement s∨ (r ∧q). If the minimal value of this expression is 1, then we know, that the argument holds. Why? Because this expression must be true under all interpretations. Therefore it follows from the first three statements.
model SAT2 "Satisfibility II";
binary variable
p "the bond market goes up";
q "interest rates decrease";
r "the stock market goes down";
s "taxes are not raised";
constraint
s1: (p or q) -> (r or s);
s2: r <-> (p and ~s);
s3: q -> (~r and ~p);
minimize s4: ~s or (r and q);
Write('%s', if (s4,'The argument is consistent','The argument is not consistent'));
end
LPL translates this statement into the following linear model:
min: + r - s;
s1: + s + r - p >= 0;
s2: + s - p + r >= 0;
s3: - r - q >= -1;
X55X: + s + r - q >= 0;
X56X: + p - r >= 0;
X57X: - p - q >= -1;
X58X: + q - s >= 0;
X59X: - s - r >= -1;
Solution
The argument is not correct.
Further Comments
Note: Williams [5] gives the following formula (22): p + q + r <= 1 for s3 which is not correct (a correct formula is produced by LPL) also formula (20) in Williams is not correct.
Questions
Verify that LPL’s translation is correct, by generating the CNF using the method given in model sat1
Verify that the argument cannot be proven with the LP relaxation.
Answers
Go to model sat1
Build the LP relaxation of the problem and solve it. The optimum is -1. This is smaller than the value of B^{(}k) which is 0. Therefore we have no proof.