Satisfibility I (sat1)

Run LPL Code  ,  PDF Document

Logical inference means to deduce logical propositions from a set of premises. The conventional way to solve logical problems is by truth tables, Boolean algebra (transformation laws), and by a well known tree searching procedure, called resolution. Another symbolic method to this inference problem is natural deduction. Still another way is to use numeric (or quantitative) methods to solve an inference problem; that is to convert the Boolean expressions into linear (or non-linear) constraints in order to prove the logical argument using mathematical programming. This has two advantages: (a) in some cases this leads to faster algorithms, (b) the analysis of the quantitative models leads to the unveiling of hidden mathematical structure. Two further advantages are: (c) symbolic (logical) and numeric (mathematical) knowledge can be mixed and represented in the same framework, (d) default or other non-monotonic knowledge can also be modeled using the same framework.

The satisfiability problem (SAT) is to decide whether a Boolean statement F follows from another statement E; or, in other words, whether E F is valid. This problem was the first problem proven to be NP-complete. The model here is a small instance of the general satisbiability problem.

One way to solve this problem using mathematical programming is to translate E and F into two CNF. From these two CNFs it is easy to build the two linear system Ax a and Bx b. Then we solve the problem:

min        x
            0
subjectto  x0e + Bx  ≥ b
           Ax  ≥ a
           x ∈ {0,1}

(where e is a column unit vector, x0 is an additional binary variable). If the minimum value x0 is 1, then E F is valid, that is, E implies F.

Another method, that does not use an additional binary x0, is to pick an arbitrary inequations (clause) within Bx b, say B(k)x b k, and to solve the linear problem

min        B (k)x
subjectto  B (i)x ≥ bi  ∀ i : i ⁄= k
           Ax  ≥ a

           x ∈ {0,1}

If B(k)x*⌉≥ b k (with the optimal solution x*), then E implies F. (LPL adopt the second method). Here is a small problem instance.

Problem

Is the following argument correct? “If fallout shelters are built, other countries will feel endangered and our people will get a false sense of security. If other countries will feel endangered they may start a preventive war. If our people will get a false sense of security, they will put less effort into preserving peace. If fallout shelters are not built, we run the risk of tremendous losses in the event of war. Hence, either other countries may start a preventive war and our people will put less effort into preserving peace, or we run the risk of tremendous losses in the event of war.” (see [1]).

Modeling Steps

  1. The following 6 Boolean propositions (binary variables) are introduced:

           p "fallout shelters are built"
           q "other countries will feel endangered"
           r "other people will get a false sense of security"
           s "other countries may start a preventive war"
           t "our people will put less effort into preserving pease"
           u "we run the risk of tremendous losses in the event of war"
          

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

  3. The second is to be formulated as: q s.

  4. The third is: r t.

  5. The fourth is: ¬p u.

  6. And the final last statement is: s t u.

We therefore have to prove E F , with :

E  ⇐ ⇒   (p →  q ∧ r) ∧ (q → s) ∧ (r →  t) ∧ (¬p → u )  and   F  ⇐ ⇒  (s ∧ t ∨ u)

Transforming the expressions into CNFs gives:

E  ⇐ ⇒  (p-∨ q) ∧ (p-∨ r) ∧ (q-∨ s) ∧ (r-∨ t) ∧ (p ∨ u)

F  ⇐ ⇒   (u ∨ s) ∧ (u ∨ t)

We choose the first clause in F :

min B (k)x    ⇐ ⇒     min  u + s

The other clause in F is B(i)x b i ⇐⇒ u + t 1

The 5 clauses in E corresponds to the five inequalities as follows:

- p + q ≥ 0,   - p + r ≥ 0,  - q + s ≥ 0,  - r + t ≥ 0,  p + u ≥ 1

The complete optimization problem is:

min        u + s
subjectto  u + t ≥ 1
           - p + q ≥ 0

           - p + r ≥ 0
           - q + s ≥ 0
           - r + t ≥ 0
           p + u ≥ 1
           p,q,r,s,t,u ∈ {0,1}

Listing 1: The Complete Model implemented in LPL [3]
model SAT1 "Satisfibility I"; 
  binary variable 
    p "fallout shelters are built"; 
    q "other countries will feel endangered"; 
    r "other people will get a false sense of security"; 
    s "other countries may start a preventive war"; 
    t "our people will put less effort into preserving pease"; 
    u "we run the risk of tremendous losses in the event of war"; 
  constraint 
    s1: p -> q and r; 
    s2: q -> s; 
    s3: r -> t; 
    s4: ~p -> u; 
  minimize 
    s5: s and t or u; 
  Write('%s', if (s5,'The argumentation is correct','The argumentation is not correct')); 
  --Write('EQU'); 
end

The IP solver finds that u + s 1 – that is the objective function is larger or equal than 1. This means that the argument is correct.

Further Comments

The common technique to solve this problem is by resolution and unification, a technique well known in logic and in logic programming languages, such as Prolog. The first step is to negate the consequence and to transform the whole statement into a conjunctive (or disjunctive) normal form, then to prove a contradiction. The CNF of E →¬F of the problem is as follows:

--
p ∨ q      (1a)
p ∨ r      (1b)
q ∨ s      (2)
--
r ∨ t      (3)
p ∨ u      (4)
s ∨ u      (5a)
t ∨ u      (5b)

A possible resolution sequence is:

which produces an empty clause, proving the contradiction. Hence the argument is valid.

Questions

  1. Verify how LPL translates these formulae into 0-1-constraints by generating the EQU-file. (Add the Instruction Write(’EQU’);).

  2. Form the LP relaxation of the linear problem generated by LPL and solve it. What do you observe?

Answers

  1. The result of LPL is the same as derived above :

            min s5:  + u + s
            s1:  + q - p >= 0
            s2:  + s - q >= 0
            s3:  + t - r >= 0
            s4:  + u + p >= 1
            X37:  + r - p >= 0
            X38:  + u + t >= 1
          

  2. Solve the following LP relaxation

    model x; 
      variable p;q;r;s;t;u; 
      minimize obj:  + u + s; 
      constraint 
        s1:  + q - p >= 0; 
        s2:  + s - q >= 0; 
        s3:  + t - r >= 0; 
        s4:  + u + p >= 1; 
        X58X:  + r - p >= 0; 
        X59X:  + u + t >= 1; 
    end

    The optimum is 1. Since we have B(k)x*⌉≥ 1 and b k = 1, we also have B(k)x*⌉≥ b k, and the argument has been proven using the LP relaxation only. By the way, all clauses are Horn clauses, therefore, the problem is solvable by the LP-relaxation.

References

[1]   Williams H.P. Logical problems and integer programming. Bull. Inst. Math. Appl., 13:18–20, 1977.

[2]   MatMod. Homepage for Learning Mathematical Modeling :  https://matmod.ch.

[3]   Hürlimann T. Reference Manual for the LPL Modeling Language, most recent version. https://matmod.ch/lpl/doc/manual.pdf.