# 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$. Commented Oct 17, 2013 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 ? Commented Oct 21, 2013 at 17:15
• @joker correct. Commented Oct 21, 2013 at 17:34