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.


1 Answer 1


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).

  • $\begingroup$ 1. Sorry, I don't know what are "equivalent lietrals". Can you point to them in your example? $\endgroup$
    – cozzie9806
    Feb 17, 2022 at 13:08
  • $\begingroup$ 2. In my thought, the process will go like this: in step 1, resolution (a or b or c) and (a' or b or c) => (b or c) // (b or c) and (b' or c) => c // c is true, and a and b can be arbitrarily assigned. $\endgroup$
    – cozzie9806
    Feb 17, 2022 at 13:13
  • $\begingroup$ 2. Well, resolution totally works. You can solve any satisfiability problem by performing all possible resolutions. But in general, there will be exponentially many steps to be performed so this is not fesable for large problems. Note that resolving two clauses with 2 variables each will result in another clause with only two (or fewer) variables. But if you resolve two clauses with 3 variables each, the resulting clause will habe 4 variables. So if you do this multiple times, your clauses will get longer and longer (and there will be exponentially many of them) $\endgroup$
    – Simon
    Feb 17, 2022 at 13:17
  • $\begingroup$ 1. My example does not have any equivlanet literals. In the context of two-sat, see here: en.wikipedia.org/wiki/… $\endgroup$
    – Simon
    Feb 17, 2022 at 13:18
  • $\begingroup$ 2. Although I resolve two clauses only when its result has at most 3 literals, does it still need exponential time? I think that the clause which has more than 3 literals will not influence to judgement for consistency. $\endgroup$
    – cozzie9806
    Feb 17, 2022 at 13:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .