2
$\begingroup$

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?

  • 0
    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.2010-12-02

1 Answers 1

5

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.

  • 0
    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.2010-12-02