[Solved]: Converting a 2-SAT formula into an implication graph

Problem Detail: 

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?

Asked By : joker

Answered By : Realz Slaw

 (¬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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/16159