Prove that 2SAT $\in$ P

computational complexitycomputer sciencenp-complete

I want to understand the proof in the following link for 2SAT $\in$ P…
What for the need of the last corollary?
Wouldn't be enought to just prove the case for the graph with the help of the path search?
Furthermore, is the proof for the corollary correct? I mean over there we have only an algorithm for a pseudo code…

Edit

About the case#2 for the Claim 2. How can we prove the contradiction? Because it seems to me that it is actually true…

I write here my thoughts:

However, since $x$ is now $FALSE$, all literals on the path from $x$ to $α$ (including $α$) must be $FALSE$. Likewise, all literals on the path from $β$ to $¬x$ (including $β$) must be $TRUE$ (because $¬x=TRUE$). This results in an edge between $α$ and $β$, with $α=FALSE$ and $β=TRUE$. Consequently the disjunction $(¬α∨β)$ becomes $TRUE$, asserting our assumption that there is a satisfactory assignment $ρ(x_1,x_2,…,x_n)$ to $Ψ$. So the contradiction fails.

Could someone tell me please what am I doing wrong?

Best Answer

Everything prior to the corollary proves that the decision problem 2SAT is in P, namely checking whether or not a 2SAT formula is satisfiable as a yes or no question. The corollary extends this result into a polynomial-time algorithm to actually find such an assignment.

As for whether or not the proof of the corollary is "correct," there's not really much of a proof to verify the correctness of. In order to be "complete," the corollary should prove the correctness (and polynomial runtime) of its proposed algorithm. Fortunately, this isn't too hard (as a hint, show that once you check a solution exists, arbitrarily assigning one variable and following the graph never introduces a conflict).

EDIT: For your follow-up question, rather than considering the path from $x$ to $\lnot x$, consider the path from $\lnot x$ to $x$. Then if $\lnot x\to \dots\to\alpha\to\beta\to\dots\to x$, we can get $\alpha$ is true, $\beta$ is false, and derive the same contradiction as in case 1.

Related Question