How to prove that adding elements to a set does not affect its satisfiability?

Question

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'$

Answer 1

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.

Answer 2

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$$

($\Rightarrow$)

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

($\Leftarrow$)

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