0
$\begingroup$

Let $F$ be a formula in CNF. Let there be a variable in $F$ called $p$ which only comes up positively( there is no $\lnot p$ in any clauses). Show that if the formula is unsatisfiable ,then we can find the empty clause using resolution by ignoring any clause where $p$ occurs.

So my idea basically is that setting $p=1$ wouldnt harm other formulas since it only comes up positively and so those clauses would be satisfied and if the formula would be unsatisfiable it would only depend on the clauses which dont have $p$, but i need some tips on how i could prove this formally.

$\endgroup$
1
$\begingroup$

Yes, you got exactly the right idea! To make this a little more formal, you should prove the following claim:

For any clause set $\Gamma$ and any variable $P$: if $P$ occurs only positively in $\Gamma$, then $\Gamma$ is satisfiable if and only if $\Gamma_P$ is satisfiable, where $\Gamma_P$ is the result of removing all clauses that contain $P$.

But yes, to prove this, you follow your idea: We know that $\Gamma$ is satisfiable if and only if either $\Gamma$ is satisfiable by setting $P$ to True, or $\Gamma$ is satisfiable by setting $P$ to False. Since by setting $P$ to True we satisfy all clauses that contain $P$, and therefore only need to satisfy $\Gamma_P$ in order to satisfy $\Gamma$ as a whole, while by setting $P$ to False we still have all clauses left to satisfy (and those that contain $P$ are now even harder to satisfy), it is strictly harder to satisfy $\Gamma$ by setting $P$ to False as compared to setting $P$ to True (put differently: whatever assignment you give to the variables other than $P$ that will satisfy all clauses in $\Gamma$ with $P$ removed from those clauses will of course also satisfy all clauses in $\Gamma_P$).

So indeed, $\Gamma$ is satisfiable if and only if $\Gamma_P$ is satisfiable, which of course means that $\Gamma$ is unsatisfiable (i.e. Empty set can be derived) if and only if $\Gamma_P$ is unsatisfiable.

By the way, such a $P$ is called a pure literal, so if you do Resolution, it is a good strategy to see if you have any pure literals (a pure literal can of course also be a case where you only have $\neg P$ for some atomic variable $P$ but no $P$'s.

$\endgroup$

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.