9 Satisfibility II (sat2)

Run LPL Code  ,  PDF Document

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

  1. 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"
          

  2. Then the first statement can be formulated as: (p q) (r s).

  3. The second then is: r (p s).

  4. The third is: q (r p).

  5. The final statement (the consequence) is: s (r q)

Hence we need to prove the following statement:

                               --          -- --      --
[((p ∨ q) → (r ∨ s)) ∧ (r ↔ (p ∧ s)) ∧ (q → (r ∧ p ))] → [s ∨ (r ∧ q)]

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.


Listing 2: The Complete Model implemented in LPL [13]
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

  1. Verify that LPL’s translation is correct, by generating the CNF using the method given in model sat1

  2. Verify that the argument cannot be proven with the LP relaxation.

Answers

  1. Go to model sat1

  2. 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.