# Is this a valid method to merge clauses in CNF formulas?

Assume $$C_1 = (x_1 \lor x_2 \lor \lnot x_3)\hspace{0.2cm} C_2 = (x_4 \lor x_5 \lor x_3) \hspace{0.2cm} C_3 = (x_3 \lor x_5 \lor x_6)$$ Let

$$\phi_1 = C_1 \land C_2 \land C_3$$ and $$\phi_2 = (x_1 \lor x_2 \lor x_4 \lor x_5) \land (x_3 \lor x_5 \lor x_6)$$

## Question

Are the two formulas $$\phi_1, \phi_2$$ equisatisfiable? Basically I have merged two clauses ($$C_1$$ and $$C_2$$) because they had a literal appearing in one and also in the other one negated. The same literal appears in the third clause $$C_3$$ which I have simply left untouched ...

## what I did

set $$x_3 = 1$$ and observed that both can be satisfied then set the variable to $$x_3 = 0$$ and observe as well that both can satisfied. So ... at least if $$\phi_1$$ is satisfiable then $$\phi_2$$ is as well ... For the reverse I can do the same here, but is it always the case ?

• Merging a conjunction of two disjunctive clauses that contain complementary literals eg: $(x \lor y) \land (\neg x \lor z) \Leftrightarrow (x \lor y) \land (\neg x \lor z) \land (y \lor z)$. The third clause $y \lor z$ is the resolvent of the first two clauses and this is called the resolution rule. In your example, $\phi_1 \Leftrightarrow C_1 \land C_2 \land \C_3 \Leftrightarrow C_1 \land C_2 \land C_3 \land resolvent(C_1, C_2) \Leftrightarrow C_1 \land C_2 \land \phi_2 C_3$.