Prove that adding a unit clause on a new atom to a set of clauses and adding its complement to clauses in the set preserves satisfiability.

I don't how to do it. Could someone give me hints to prove it? Or the sketch of the proof? please?

In my desperate attempts I tried to visualize with a particular example:

Consider $S=\{p,q\}$, we assume it satisfiable under $v$, i.e. $v(p)=true\ and\ v(q)=true$. Now we create the new set $S'=\{\{r\},\{pq\overline r\}\}$ and we have to show that is satisfiable under $v$ too. But the valuation $v$ doesn't have $r$ as domain. What to do in this case? It is supposed that $v$ must be the same valuation for $S$ and $S'$

  • 1
    $\begingroup$ The claim you need to prove is that the new set of clauses is satisfiable if and only if the original set of clauses is satisfiable. In case both sets are satisfiable, the valuation for the new set of clauses is not the same, as you noted, as the valuation for the original set, because it also gives a value to the new atom. Which value? (It should not be difficult to see.) $\endgroup$ – Fabio Somenzi Mar 30 '18 at 19:11
  • $\begingroup$ @FabioSomenzi oh ok $v(r)=true$. $\endgroup$ – user178403 Mar 30 '18 at 19:21
  • $\begingroup$ It is always $v(r) = \mathit{true}$. What you need to do next is to show that this choice makes the new set of clauses satisfiable if and only if the original set is satisfiable. If the original set is satisfiable, you just augment a valuation that witnesses its satisfiability with $v(r)$. Otherwise, you need to argue that under both $v(r) = \mathit{true}$ and $v(r) = \mathit{false}$, the new set is unsatisfiable. $\endgroup$ – Fabio Somenzi Mar 30 '18 at 19:26
  • $\begingroup$ BTW, your example does not seem right. If $S$ is a set of two unit clauses, you should write it $\{\{p\},\{q\}\}$. Then $S' = \{\{p,\bar{r}\}, \{q,\bar{r}\}, \{r\}\}$. $\endgroup$ – Fabio Somenzi Mar 30 '18 at 19:29
  • $\begingroup$ @FabioSomenzi Ok I get the idea, but I don't know how to write the proof for the generalize case? $\endgroup$ – user178403 Mar 30 '18 at 19:36

See Ben-Ari, page 29:

Let $A$ a formula: $A$ is satisfiable iff $v_I (A) = \text{T}$ for some interpretation $I$ [where $v_I(A)$ is the truth-vale of $A$ under $I$].

Thus, if $A$ is a clause that is satisfiable, like e.g. $p \lor q$, this means that there is an interpretation $I$ such that $v_I(p \lor q) = \text{T}$.

Recall that [page 16] :

An interpretation for a formula $A$ is a total function $I : P_A \to \{ \text T, \text F \}$ [where $P_A$ is the set of atoms appearing in $A$; in the case above : $P_A = \{ p,q \}$] that assigns one of the truth values $\text T$ or $\text F$ to every atom in $P_A$.

If we get a new unit clause [page 77 : a literal] $r$, we have that $r \notin P_A$ and thus the interprettaion $I$ is not defined for it.

Thus, we have to extend $I$ to $I' : \{ p,q,r \} \to \{ \text T, \text F \}$.

The new set of clauses is : $\{ \{p, q, \lnot r \}, \{ r \} \}$; obviously, we need $I'(r)= \text T$. But the fact that $v_{I'}(\lnot r)= \text F$ does not affect the satisfiabiliy of $p \lor q \lor \lnot r$.

Conclusion: having found an interpretation $I'$ that satisfy the new set of clauses, we have proved tha fact that the "procedure" described above does not affect satisfiability.

  • $\begingroup$ This is very clear, thank you! :) $\endgroup$ – user178403 Apr 7 '18 at 4:24
  • $\begingroup$ Although this is for the case $p\lor q$, Can I use induction on the length of the formula $A$ to prove in general? For instance, Can I say let's see if the statement holds for n=2 which is for $p\lor q$ ... thus the result hold. Therefore the result must also hold for the formula $A$ of length $n$ ? $\endgroup$ – user178403 Apr 7 '18 at 4:29
  • $\begingroup$ @Michelle - Yes, obviously. The key point in that a clause is a disjunction and if it is satisfiable, adding a new false disjunct does not affect satisfiability. $\endgroup$ – Mauro ALLEGRANZA Apr 7 '18 at 7:52

I suggest you think in terms of formulas, not clauses.

It seems that your statement considers CNFs because for DNFs it holds only in one direction (it is an easy exercise to show this).

Now, recall that a set of CNF clauses $$\{\{p^1_1,\ldots,p^1_n\},\ldots,\{p^m_1,\ldots,p^m_n\}\}$$ is the same thing as $$\bigwedge\limits^{m}_{i=1}\bigvee\limits^{n}_{j=1}p^i_j$$

So, in terms of formulas we want to show the following. $$\exists v:v(\bigwedge\limits^{m}_{i=1}\bigvee\limits^{n}_{j=1}p^i_j)=1\Leftrightarrow\exists v':v'(\bigwedge\limits^{m}_{i=1}(\bigvee\limits^{n}_{j=1}p^i_j\vee\neg q)\wedge q)=1$$


Assume that $\bigwedge\limits^{m}_{i=1}\bigvee\limits^{n}_{j=1}p^i_j$ is satisfiable.

This meanst that for every $i$ $\bigvee\limits^{n}_{j=1}p^i_j$ is satisfiable by $v$. Now, extend $v$ to $v'$ setting $v'(q)=1$. Obviously $v(\bigwedge\limits^{m}_{i=1}(\bigvee\limits^{n}_{j=1}p^i_j\vee\neg q)\wedge q)=1$.


Assume $w(\bigwedge\limits^{m}_{i=1}(\bigvee\limits^{n}_{j=1}p^i_j\vee\neg q)\wedge q)=1$. Obwviously, $w(q)=1$ and $w(\neg q)=0$. Recall that $w$ satisfies $\bigwedge\limits^{m}_{i=1}(\bigvee\limits^{n}_{j=1}p^i_j\vee\neg q)$. This means that for every $i$ $w(\bigvee\limits^{n}_{j=1}p^i_j\vee\neg q)=1$. From here follows that $w(\bigvee\limits^{n}_{j=1}p^i_j)=1$.


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.