2
$\begingroup$

I don't 100% understand this. But I have a entailment, and I want to prove whether it is satisfiable or not, and I will do this using resolution and variable elimination.

Here is the formula: $$ (x_1 \lor x_2 \lor x_6) \land (\lnot x_1 \lor x_3 \lor x_8) \land (\lnot x_2 \lor \lnot x_3 \lor x_4) \land \\ (\lnot x_4 \lor x_5 \lor x_7) \land (\lnot x_4 \lor x_6 \lor x_8) \land ( x_5 \lor \lnot x_6) \land \\(\lnot x_6 \lor x_7 \lor \lnot x_8) \land (x_7 \lor \lnot x_8 \lor \lnot x_{10}) \vDash \lnot(x_7 \lor \lnot x_9 \lor x_{10}) $$ First I negate the conclusion and move it into the premises. If I can prove this to be ⊥ using Resolution, I have proven that the original entailment IS satisfiable. So this is what I want to refute by using resolutin (and variable elimination to simplify).

$$ (x_1 \lor x_2 \lor x_6) \land (\lnot x_1 \lor x_3 \lor x_8) \land (\lnot x_2 \lor \lnot x_3 \lor x_4) \land \\ (\lnot x_4 \lor x_5 \lor x_7) \land (\lnot x_4 \lor x_6 \lor x_8) \land ( x_5 \lor \lnot x_6) \land \\(\lnot x_6 \lor x_7 \lor \lnot x_8) \land (x_7 \lor \lnot x_8 \lor \lnot x_{10}) \lor (x_7 \lor \lnot x_9 \lor x_{10}) $$

So I start off by eliminating all clauses with $x_7$ since it's a pure literal, which leaves me with

$$ (x_1 \lor x_2 \lor x_6) \land (\lnot x_1 \lor x_3 \lor x_8) \land (\lnot x_2 \lor \lnot x_3 \lor x_4) \land \\ (\lnot x_4 \lor x_6 \lor x_8) \land (x_5 \lor \lnot x_6) $$

Here $x_5$ is a pure literal, so that one clause can be removed.

$$ (x_1 \lor x_2 \lor x_6) \land (\lnot x_1 \lor x_3 \lor x_8) \land (\lnot x_2 \lor \lnot x_3 \lor x_4) \land (\lnot x_4 \lor x_6 \lor x_8) $$

Now $x_6$ is a pure literal, which would leave just the two clauses

$$ (\lnot x_1 \lor x_3 \lor x_8) \land (\lnot x_2 \lor \lnot x_3 \lor x_4) $$

However, here $x_8$ is a pure literal, thus leaving us with only one clause, and that clause contains pure literals. Can it really be simplified into nothing? It feels like I'm doing something wrong but I'm not sure what it is that's wrong.

If I really can simplify into nothing, would that mean that the original formula is satisfiable or not satisfiable?

Since all the clauses contain a pure literal, wouldn't that make it impossible to resolve?

$\endgroup$
2
  • $\begingroup$ You seem to have replaced $x_1 \lor x_2$ with $x_1 \lor x_2 \lor x_6$, as well as $\lnot x_5 \lor \lnot x_6$ with $x_5 \lor \lnot x_6$. $\endgroup$ May 27, 2021 at 13:14
  • $\begingroup$ You are right, I edited it to be correct. Thanks. $\endgroup$
    – Fearvik
    May 27, 2021 at 13:22

1 Answer 1

0
$\begingroup$

If $x_7$ is a pure literal, then this means that you can satisfy all clauses containing $x_7$ by setting it to true. Accordingly, we set $x_7,x_5,x_6,x_8$ to true, satisfying all clauses apart from $\lnot x_2 \lor \lnot x_3 \lor x_4$, which we can satisfy by setting $x_4$ to true (for example).

If you set $x_4,x_5,x_6,x_7,x_8$ to true, then the left-hand side of your original formula is satisfied (once you correct $x_1 \lor x_2$ to $x_1 \lor x_2 \lor x_6$ and $\lnot x_5 \lor \lnot x_6$ to $x_5 \lor \lnot x_6$), while the right-hand side is falsified, and so the entailment is false. (In contrast to your post, there is no "formula" there which can be satisfied or not.)

$\endgroup$
15
  • $\begingroup$ Okay! Thank you for the answer. What I was trying to do was to prove whether the entailment is satisfiable, and I wanted to prove it using resolution + variable elimination. Moving the conclusion to the premises and then proving ⊥ using resolution would prove that the original entailment would be satisfiable. I'm just not quite sure how to prove it using Resolution. $\endgroup$
    – Fearvik
    May 27, 2021 at 13:37
  • $\begingroup$ Also I really appreciate the edit you made to my post, thank you! :) $\endgroup$
    – Fearvik
    May 27, 2021 at 13:38
  • $\begingroup$ You're checking whether the entailment is refutable, not satisfiable. $\endgroup$ May 27, 2021 at 13:56
  • $\begingroup$ Resolution is a refutation system. It can prove that the entailment always holds, which isn't the case here. $\endgroup$ May 27, 2021 at 13:57
  • $\begingroup$ I'm following this cs.uwaterloo.ca/~cbruni/CS245Resources/lectures/2018_Fall/… at page 18. It says that if you negate the conclusion and convert it into CNF, and then refute that using Resolution, that means that the entailment is satisfiable. $\endgroup$
    – Fearvik
    May 27, 2021 at 13:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.