Satisfiability proof of formulas with pure literals

547 Views Asked by At

Let $\varphi$ be any propositional formula in negation normal form (NNF). A literal $\ell$ is pure in a formula $\varphi$, if the complement of $\ell$, $\ell^c$, does not occur in $\varphi$, where $\ell^c$ is $b$ if $\ell$ is $\neg b$ and $\ell^c$ is $\neg b$ if $\ell$ is $b$.

I have to prove that: If $\varphi$ contains only pure literals, then $\varphi$ is satisfiable.

I decided to prove this by structural induction over the definition of well formed NNF formulas:

Let $P(\varphi)$ denote the statement that $\varphi$ is satisfiable.

Base Case: $\varphi = a$. Then $P(\varphi)$ holds trivially because a formula which only consists of a single literal is trivially satisfiable.

Induction Hyp.: Let $\varphi$ be a formula in NNF with $n$ literals and assume $P(\varphi)$ holds.

Step Cases: $\psi := \varphi \land \ell$: By induction hyp, $\varphi$ does only contain pure litarals and $P(\varphi)$ holds. If we add another pure literal as conjuct to $\varphi$, $\psi$ stays satisfiable, since $\ell$ is a pure literal (i.e. $\ell^c$ does not occur in $\varphi$).

I believe that until here my proof structure is correct. However, can anybody help me out with the step cases? I know that I need to show it for formulas of the kind $\neg \psi$,$\psi \land \phi$, and $\psi \lor \phi$ Can anybody explain how to proceed with one of the step cases?

1

There are 1 best solutions below

1
On

Overview: if $\phi$ is a pure formula, in the sense of your question, and $v$ is a propositional variable in $\phi$, define an assignment that makes $v$ true if $v$ is not negated in $\phi$ and makes it false if $v$ is negated. This is possible by the definition of pure formula and will make all the literals in the formula true. As negation only appears in literals in a formula in NNF, your formula is now formed from true literals using conjunction and disjunction, hence it is satisfied by this assignment.

Details of the structural induction: you haven't got the steps in your framework quite right. In the step for $\land$ you have pure formulas $\phi$ and $\psi$ and you have to prove that if $\phi \land \psi$ is pure, then it is satisfiable. You can assume that $\phi$ and $\psi$ are satisfied by the assignment decribed above. Let's say those assignments are $\alpha$ for $\phi$ and $\beta$ for $\psi$. You may also assume that $\phi \land \psi$ is pure, which implies that $\alpha$ and $\beta$ agree on variables that appear free in both $\phi$ and $\psi$, hence $\alpha \cup \beta$ is the assignment described above and it makes both $\phi \land \psi$ hold. Similarly for $\phi \lor \psi$. In the step for $\lnot$, you are given $\phi$ and that $\lnot \phi$ is pure, which means that $\phi$ must be a variable $p$ say. The assignment described above for $\lnot p$, make $p$ false and hence makes $\lnot p$ hold and we are done.

If you really want to dig into the fine details, my informal description of the satisfying assignment needs to be replaced by a formal definition by recursion over the structure of the formula. That is far more detail than one would usually expect to see in a proof in the literature.