0
$\begingroup$

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 ?

follow up

Is this merging always possible? i.e merge two clauses in a CNF like so, if they share a variable which negated in one as opposed to another.

Improve this question
$\endgroup$
4
  • $\begingroup$ 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$. $\endgroup$
    – vvg
    Mar 9 at 9:54
  • $\begingroup$ I am not necessarily asking for logical equivalence ... I am "satisfied" with just equisatisfiability with the advantage that I have reduced the number of clauses. I am not necessarily interested in their size. $\endgroup$
    – C Marius
    Mar 9 at 9:59
  • $\begingroup$ If you use the resolution rule, you get equivalence. Equivalence gives you equisatisfiability (not vice versa). $\endgroup$
    – vvg
    Mar 9 at 10:02
  • $\begingroup$ I think two formulas can be equisatisfiable but not equivalent see en.wikipedia.org/wiki/…. Equivalence is too much for me here $\endgroup$
    – C Marius
    Mar 9 at 10:07

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.