Explanation of conversion of CNF to imperative normal form in 2-SAT problem?

Question

so this question might seem dumb to many of you but I'm finding it somewhat hard to grasp the conversion of a CNF clause to INF one.

I was going through this article where it states:

First we need to convert the problem to a different form, the so-called implicative normal form. Note that the expression a∨b is equivalent to ¬a⇒b∧¬b⇒a (if one of the two variables is false, then the other one must be true).

Can somebody explain how do we get to this result/how does this conversion makes sense? I've no idea what that " => " sign means, either. Thanks in advance!

Update 1: If in doubt with different logical symbols, refer to this wiki.

Answer 1

=> is implication, with the truth table:

A B | A => B
----+-------
F F |   T
F T |   T
T F |   F
T T |   T

In fact, you can show that a => b is equivalent to ~a \/ b. (Just fill out the truth tables.)

Now, we have:

  ~a => b 
= ~(~a) \/ b
= a \/ b

So, it's even stronger: a \/ b is equivalent to ~a => b. You can similarly show it is also equivalent to ~b => a; so taking the conjunction is redundant perhaps, but it doesn't change the equivalence.

If in doubt, always draw the full truth tables, assuming you have 4-5 variables it would be very educational. If you have more variables, use a SAT/SMT solver to prove equivalence. That's what they are good for.