Proving satisfiability using resolution and variable elimination

Question

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?

Answer 1

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