satisfiability2-satisfiabilityproof-system

Derivation in the Resolution Proof System


The clauses of our problem: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}

How can we conclude from these clauses to {}?

I can see that this cannot be satisfied, but I am unable to find a solution in the Resolution Proof System as it seems that [{x,y},{{¬x,¬y}] results in {x,y,¬y} or {y,x,¬x} and then we can derive {x,¬x} and {y,¬y}. It seems that this is obvious as (T or F) will be always T.

I know that this is not satisfiable because there is no solution that satisfies the problem.


Solution

  • You can apply Davis-Putnam. This applies resolution in an exhaustive fashion that eliminates propositional variables one at a time. It is a complete method that is able to deduce {} iff a propositional CNF formula is unsatisfiable.

    Here is a good introduction https://www.fi.muni.cz/~popel/lectures/complog/slides/davis-putnam.pdf . To produce the proof one just needs to track the resolutions it does that contribute to the final derivation.

    For this problem if you apply it in the order x, y, z one gets the proof:

     1. {x,y}   . input
     2. {x,z}   . input
     3. {y,z}   . input
     4. {~x,~y} . input
     5. {~x,~z} . input
     6. {~y,~z} . input
     7. {y,~z}  . resolve(x, 1, 5)
     8. {~y,z}  . resolve(x, 2, 4)
     9. {~z}    . resolve(y, 7, 6)
    10. {z}     . resolve(y, 3, 8)
    11. {}      . resolve(z, 10, 9)