# Help understanding the proof that 2SAT is in P

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?

-
Does + here mean "or"? That's confusing. – Qiaochu Yuan Dec 2 '10 at 12:45
In your example, we reach a contradiction setting $x$ to true, so we set $x$ to false instead, which forces $y$ to be true, and we are done. – Qiaochu Yuan Dec 2 '10 at 12:58
@Qiaochu: I changed the notation. I agree that flipping x will work, but I do not understand how this can always be in P. If we brute force it, there would be $2^n$ tries. Suppose each var implies one other. Then this would reduce it to only $2^{n/2}$, right? – Xodarap Dec 2 '10 at 14:04
it is actually impossible for each variable to only affect one other variable. Try it yourself on a bigger example. – Qiaochu Yuan Dec 2 '10 at 14:39
The disjunction in your second clause should go to $x\implies\bar{x}$, which should correspond to $\bar{x}$, but I don't know if you have that rule. – Ross Millikan Dec 2 '10 at 15:18

The graph in the paragraph you're quoting is the transitive closure of the original graph. Your algorithm can be adapted as follows: choose an arbitrary literal $\alpha$ and make all the necessary assignments; if you reach $\lnot \alpha$ (or reach both $\beta$ and $\lnot \beta$ for some other variable $\beta$), then $\alpha$ must be false, so try again from $\lnot \alpha$; if you reach $\alpha$ (or reach both $\beta$ and $\lnot \beta$ for some other variable $\beta$), then the instance is unsatisfiable. Continue until you set the values of all variables.
So suppose we set x. Then try y and $\neg y$, both lead to some $z \wedge \neg z$. Won't we then try $\neg x$, then y and $\neg y$ again, etc.? Or are you saying that if $x \wedge (y \vee \neg y)$ leads to a contradiction, $\neg x \wedge (y \vee \neg y)$ must also? – Xodarap Dec 2 '10 at 16:44
Suppose first $x \Rightarrow z$. If then both $y \Rightarrow \lnot z$ and $\lnot y \Rightarrow \lnot z$ then there's no satisfying assignment. So suppose given $x$, both $y$ and $\lnot y$ imply $z$ and $\lnot z$. Again we get that there's no satisfying assignment. The scenario you're thinking of can only happen if there's a clause with at least $3$ variables - in 2SAT the implications are independent since the clauses are so small. – Yuval Filmus Dec 2 '10 at 18:18