Why doesn’t Krom’s method apply to solving the 3SAT in polynomial time

algorithmsconjunctive-normal-formnp-completesatisfiability

In the paper "The Decision Problem for a Class of First-Order Formulas in Which all Disjunctions are Binary", Krom suggested a method to solve 2SAT problem.

My understanding is this.

  1. Use resolution and unit propagation to deduce other clauses.
  2. If there are remaining variables despite of repeated actions in 1, assign any truth value to one remaining variable, and go to 1.
  3. If all variables have truth values, then the process is completed.

It seems that this process can be applied to 3-CNF with little modification. It is that actions in 1 must be done when the result clause has at most 3 literals. ex) (a or b or c) and (a' or b or d) => (b or c or d)
This will soon make clauses that have 2 literals or 1 literal. If not, any variable is assigned truth value.

I wonder whether this Krom's method works well in polynomial time.

Best Answer

First: Your understanding of the 2SAT solution is incomplete. Before doing the three steps you, have to compute "equivalent literals" (using any linear-time algorithm for strongly connected components). Otherwise it will generally not work.

Secondly: You can certainly apply these steps to 3SAT. In fact, there are many computer programs for solving general satisfiability problems, and these are the basic steps, usually called "unit propagation" and "branching".

The problem appears if this procedure gets to a point where you have found a contradiction (i.e., you have to assign both "true" and "false" to a variable).

In the case of 2SAT (after removing equivalent literals), this means that the problem definitely has no solution (it is "unsatisfiable").

In 3SAT (or larger general satisfiability), this does not need to be the case. You have to go back to a previous assignment (step 2 in your question), and try out the other assignment (this is called "backtracking"). Only after you checked all possibilieties can you be sure that there is no solution. And generally there are exponentially many combinations of these decisions, which makes the approach exponentially slow in general (though there are amazing heuristics that can improve this A LOT for many practical cases).

Here is an example: Suppose you have the three clauses

$(a\vee b\vee c)$ and $(\neg a\vee b\vee c)$ and $(\neg b \vee c)$

If you arbitrarily decide to set $c=\text{false}$, it will follow (from the third clause) that $b=\text{false}$. And the first and second clauses become $(a)$ and $(\neg a)$, which is a contradiction. But it would be incorrect to conclude that the whole formula does not have a solution (for example $a=b=c=\text{true}$ works).

Related Question