I have seen this thread.
However, I don't understand the answers. Following problem with the 2nd answer (the one of MGwynne):
He says that the number of clauses is quadratic of $n$ (the number of variables). I see that (this way: a clause has 2 variables, they can be put together with $\wedge$ and $\vee$. Each variable can also have a $\neg$ before it. So we get $2*2*2*\binom{n}{2}$ (because $\wedge$ and $\vee$ are commutative we don't need permutations). Which is in $O(n^2)$).
But I don't see how we conclude that $2SAT$ is in $P$. How can we determine whether there is a satisfying solution for a single clause? We cannot just iterate over the potential solutions, as that would be $2^n$ which is not polynomial.
Best Answer
Consider some literal $x$ in formula $\phi$. If there is a clause with only one literal $x$, and a clause with only one literal $\lnot x$, the formula is not satisfiable. If $x$ is always positive or always negative, you can remove all the clauses containing $x$. Otherwise, $x$ appears in clauses $x \lor a_1, \ldots, x \lor a_k$ and $\lnot x \lor b_1, \ldots \lnot x \lor b_{k'}$. What we can do is replace all these clauses using $x$ by the following clauses: $a_i \lor b_j$ for all $i \in \{1,\ldots,k\}$ and $j \in \{1,\ldots,k'\}$. Those together with all the clauses not containing $x$ or $\lnot x$, and after simplifying all the trivial clauses and the redundancies, makes a new formula $\phi'$ without the variable $x$.
If the formula $\phi$ was satisfiable, so is the new formula $\phi'$. Indeed, say it was satisfiable by some assignment where $x$ is true, then $b_j$ must be true for all $j$, hence $\phi'$ is satisfiable. Similarly if $x$ is false, $a_i$ is true and $\phi'$ is satisfied.
Reciprocally, if $\phi'$ is satisfiable, so is $\phi$: consider an satisfying assignment for $\phi'$. Then either all $a_i$ must be true, or all $b_j$ must be true (if not, then some clause in $\phi'$ is not satisfied).
By this procedure, we remove one variable while keeping the same satisfiability status. After $n$ steps, where $n$ is the number of variables, we will have determined whether $\phi$ is satisfiable.
This procedure is actually just a Fourier-Motzkin elimination, in the context of boolean algebra. You can also apply it for more general SAT formulas (consider this as an exercise). But the 2SAT formulas behave well for it, because each step transforms a 2SAT formula into another 2SAT formula with one less variable. If you apply it to a 3SAT formula, you will get a 4SAT formula, and so on. In general, Fourier-Motzkin elimination generates exponentially many linear terms. Here because we stay in 2SAT, we only ever get a polynomial number of clauses (the $O(n^2)$ that you refer to), which ensures the polynomiality of this algorithm.
Notice that this is not the most efficient algorithm for 2SAT, it is only one of the simplest.