# Converting a 2-SAT formula into an implication graph

Both wikipedia and my lecturer explained how the 2 satisfiability problem work. However, I am finding it really hard understanding how this formula:

xvy≡ ¬x-->y ≡ ¬y -->x


Then breaks down the following conjectures :

(¬x v y) & (¬y v z) & (¬z v w) & (¬w v ¬x) &
(x v ¬y) & (y v ¬z) & (z v ¬w) & (w v x)


is converted to an implcation graph.

Heres my attempt:

 (¬x v y) = (¬y-->x)

= (¬x-->y)


but this cannot be right, as they have diffrent truth tables:

(¬y-->x)


1 0 0 0

1 0 1 1

0 1 1 0

0 1 1 1

(¬ x-->y)


1 0 0 0

0 1 1 1

1 0 0 0

0 1 1 1

I understand once you have the conjectures converted to implication, how to construct the implication graph and find out if its not satisfiable (bad loops).

Could someone please explain clearly how to break down the conjectures to implications?

• Your first conversion is wrong. $\neg x \vee y$ is equivalent to $x\to y$ and to $\neg y\to \neg x$. – Shaull Oct 17 '13 at 14:19

 (¬x v y) = (¬y-->x)


\begin{align} \text{rule: } &A \vee B &=& (\neg A \implies B)\\ & \neg x \vee y &=& (\neg\neg x \implies y)\\ & &=& (x \implies y) &(1)\\ \end{align}

          = (¬x-->y)


So now this becomes:

\begin{align} \text{rule: } &A \implies B &=& (\neg B \implies \neg A)\\ &(x \implies y) &=& (\neg y \implies \neg x) & (2) \end{align}

And we get:

\begin{align} (x \implies y) & (1)\\ (\neg y \implies \neg x) & (2) \end{align}

And the truth table:

$$\left.\begin{array}{rrrr} x & y & (\neg x \vee y) & (x \implies y) & (\neg y \implies \neg x) \\ 0 & 0 & 1 & 1 & 1 \\ 0 & 1 & 1 & 1 & 1 \\ 1 & 0 & 0 & 0 & 0 \\ 1 & 1 & 1 & 1 & 1 \\ \end{array}\right.$$

As you can see they are equivalent.

• Am i correct in saying for the second conjecture : (¬y v z) The implications for this is: y-->z, ¬z -->¬y ? – joker Oct 21 '13 at 17:15
• @joker correct. – Realz Slaw Oct 21 '13 at 17:34