I have read this paper and the wikipedia summary here and even this homework problem, but I do not understand how 2SAT is in P.
Here is my concern: the idea is that we start by setting a random variable. Then we set any implied variables. Repeat, and if we eventually reach a contradiction, then the problem has no solution. For example, that homework solutions thing says:
Begin with an arbitrary vertex α such that (α, ¬α) is not an edge in the graph. [Fill out implied variables]. Repeating this process for every unassinged literal in I creates a satisfying assignment.
I do not think this is always works. Take $(x\vee y)\wedge(\bar{x}\vee\bar{x})$. Set x = true. Now the second clause doesn't work, and we've reached a contradiction. But this formula does have a solution: $\bar{x}\wedge y$. Yet if we look at the implication for the second clause, it is $x\implies x$, so it's not as though we didn't set an implied variable. There is no rule $x\implies\bar{x}$ either, so it doesn't contradict that constraint.
This link says to "rewind" once if you reach a contradiction, but I don't see why it's not possible to reach contradictions any number of times even if the proposition is satisfiable.
What am I missing here?