4
$\begingroup$

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?

$\endgroup$
5
$\begingroup$

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).

$\endgroup$
2
$\begingroup$

The arrows symbolize material implication, which is the operator with the truth table

$$\begin{matrix} A & B & A\Rightarrow B \\ \hline 0 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 0 & 0 \\ 1 & 1 & 1 \end{matrix}$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.