I am trying to convert the following conjectures to implications to then draw the implication graph.
The conjectures are: {¬x,y}, {¬y,z}, {¬z,w} ,{¬w,u},{¬u,¬x},{x,w},{¬w,x}
I converted the conjectures into implications so I could construct the implication graph:
{¬x,y}: I have x-->y and ¬x -->¬y
{¬y,z} : I have y-->z and ¬y-->¬z
{¬z,w} : I have z-->w and ¬z-->¬w
{¬w,u} : I have w-->u and ¬w--->¬u
{¬u,¬x} : I have u-->¬x and ¬x-->¬u
{x,w} : I have ¬x-->w and ¬w-->x
{¬w,x} : 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.
I would argue that these conjectures 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!
I'm not usually giving a full answers, but this is quite complicated, so I will provide all the details. Please work it out yourself again, perhaps for another formula, to check if you understand it.
For clause $\{l_1, l_2\}$ the implications should be $\neg l_1 \to l_2$ and $\neg l_2 \to l_1$. You do this correctly for e.g.
but incorrectly for e.g.
where it should be $x \to y$ (correct) and $\neg y \to \neg x$ (different). Another method to do this is to use transposition, i.e. $P \to Q \iff \neg Q \to \neg P$. The idea behind this is that 2SAT requires all the clauses to be true, so for a clause $\{l_1, l_2\}$ to be true, if $l_1$ fails then $l_2$ has to be true, and if $l_2$ fails, then $l_1$ has to be true.
If I didn't make any typos, then the graph would look like below, and you can clearly spot an inconsistency with $w \to x \to \neg u \to \neg w$ and $\neg w \to x \to y \to z \to w$. The point is that formula cannot be satisfied if it implies that some variable has to be both true and false. In other words you should look for cycles that have both $\alpha$ and $\neg \alpha$ where $\alpha$ is any of your variables (in this case $\alpha \in \{x,y,z,u,w\}$).
I hope this helps $\ddot\smile$