10 Satisfibility III (sat3)

Run LPL Code  ,  PDF Document


Is the following set of statements correct? “If Superman were able and willing to prevent evil, he would do so. If Superman were unable to prevent evil, he would be impotent and if he were unwilling to prevent evil, he would be malevolent. Superman does not prevent evil. If Superman exists, he is neither impotent nor malevolent. Therefore, Superman does not exist.” (see [4]).

Modeling Steps

  1. We introduce 6 Boolean propositions as follows:

              a  "Superman is able to prevent evil"
              w  "Superman is willing to prevent evil"
              i  "Superman is impotent"
              m  "Superman is malevolent"
              p  "Superman prevents evil"
              e  "Superman exists"

  2. Then the first statement can be formulated as: a w p.

  3. The second is: (a i) (w m).

  4. The third is: p.

  5. The fourth is: e i m.

  6. The last statement (the consequence) is: e.

Hence, we need to show the following Boolean expression:

                --        --        --       ------      --
[(a ∧ w → p ) ∧ (a → i) ∧ (w →  m ) ∧ p ∧ (e → i ∨ m )] → (e)

Listing 3: The Complete Model implemented in LPL [13]
model SAT3 "Satisfibility III"; 
  binary variable 
    a "Superman is able to prevent evil"; 
    w "Superman is willing to prevent evil"; 
    i "Superman is impotent"; 
    m "Superman is malevolent"; 
    p "Superman prevents evil"; 
    e "Superman exists"; 
    s1:  a and w -> p; 
    s2:  (~a -> i) and (~w -> m); 
    s3:  ~p; 
    s4:  e -> i nor m; 
  minimize ne: ~e "Superman does not exist"; 
  Write('%s', if (e,'Superman exists.','Superman does not exist')); 


The Boolean statement is correct, that is, the argumentation is correct and unfortunately, Superman does not exist.


  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.


  1. The LPL translation is as follows

       min:   -e; 
       s1:     p - w - a >= -1; 
       s2:     i + a >= 1; 
       s4:    -i - e >= -1; 
       X56X:   m + w >= 1; 
       X57X:  -m - e >= -1;
  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.