# 2-SAT implication Understanding

Having a simple 2-SAT problem where the equation is simply: $a \lor b$

We have two implications:

$\lnot a \Rightarrow b$
$\lnot b \Rightarrow a$

Thus, in the graph we build we add edges similar to the arrows above.

What exactly do the arrows symbolise in this instance? I've read that they means if $a$ is true, $b$ must be true as well. The same for false. Why can we model this equation in such a way?

You are asking why we can model the equation $a \lor b$ as two directed edges in a graph. The answer is that mathematics is a free country, and we are allowed to do whatever we want. The only restriction we have to obey is that whenever we claim a result, it must be accompanied by a valid proof.
This representation is used in an algorithm that decides whether a 2SAT instance is satisfiable. As you mention, an edge from a literal $\ell_1$ to a literal $\ell_2$ means that if $\ell_1$ is true, then $\ell_2$ has to be true. Indeed, if $a \lor b$ holds then if $\lnot a$ is true, $b$ must be true, and vice verse, if $\lnot b$ is true, $a$ must be true.
If there is a path from some literal to its negation – from $x$ to $\lnot x$ or from $\lnot x$ to $x$, for some variable $x$ – then clearly the formula is not satisfiable, since $x$ cannot be both true and false. A more delicate argument shows that if no such paths exist, then the formula is satisfiable. This is proved by showing how to find a satisfying assignment for the formula (it's a nice exercise).
$$\begin{matrix} A & B & A\Rightarrow B \\ \hline 0 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 0 & 0 \\ 1 & 1 & 1 \end{matrix}$$