1
$\begingroup$

I am trying to convert the following 2-sat clauses to implications and then draw the implication graph.

The clauses are: {¬xvy}, {¬yvz}, {¬zvw} ,{¬wvu},{¬uv¬x},{xvw},{¬wvx}

I converted the boolean literals into implications so I could construct the implication graph:

{¬xvy}: I have x-->y and ¬x -->¬y

{¬yvz} : I have y-->z and ¬y-->¬z

{¬zvw} : I have z-->w and ¬z-->¬w

{¬wvu} : I have w-->u and ¬w--->¬u

{¬uv¬x} : I have u-->¬x and ¬x-->¬u

{xvw} : I have ¬x-->w and ¬w-->x

{¬wvx} : I have w-->x and ¬w-->¬x

Am I doing this right? If so, I have constructed this implication graph to prove it is not satisfiable.

enter image description here

I would argue that these literals are not satisfiable because of the infinite loops you can have from ¬w ¬x ¬y ¬z ¬w and w x y z w. Is this a sufficient enough explanation?

Thanks in advance!

$\endgroup$
  • $\begingroup$ How is a set of two boolean literals a conjecture? I don't understand the semantics, especially since the sets aren't ordered. $\endgroup$ – G. Bach Oct 21 '13 at 19:04
  • $\begingroup$ okay the comma denotes or's i will edit $\endgroup$ – joker Oct 21 '13 at 19:12
2
$\begingroup$

{¬uv¬x} : I have u-->¬x and ¬x-->¬u

LMFTFY:

$$(\neg u \vee \neg x) = \left[(u \implies \neg x) \wedge (x\implies \neg u)\right]$$

{¬wvx} : I have w-->x and ¬w-->¬x

LMFTFY:

$$(\neg w \vee x) = \left[(w \implies x) \wedge (\neg x\implies \neg w)\right]$$

From this you get the following graph:

enter image description here

graphviz source

And the strongly connected components (there is only one):

enter image description here

graphviz source

And we get $\left\{u,\neg u,w,\neg w, x,\neg x,y,z,\neg z\right\}$, obviously a contradiction (the elements of this set implies each-other).

I would argue that these literals are not satisfiable because of the infinite loops you can have from ¬w ¬x ¬y ¬z ¬w and w x y z w. Is this a sufficient enough explanation?

It isn't the "infinite" loops that make it unsatisfiable. "infinite loops" or cycles, make strongly connected components; and a 2sat formula is satisfiable iff (if and only if) there are no contradicting terms in any of its strongly connected components. In this graph there are clearly contradicting terms in the one large strongly connected component, as I demonstrated above, therefore it is unsatisfiable.

$\endgroup$
  • 1
    $\begingroup$ LMFTFY - "let me fix that for you" $\endgroup$ – Julian A. Jan 20 '17 at 22:39

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.