Why can $2$-SAT be solvable efficiently, but $3$-SAT not?

Question

I am aware that 2SAT is polynomial while 3SAT is not, but I am looking for an intuition why its so. After all, even in 2SAT we can attempt all possible truth functions and its $2^n$. So I am hoping not for a formal proof, but for intuition or explanations that distinguishes the language from 3SAT?

Answer 1

As was mentioned in a comment we can only say that 3SAT is NP-hard. In 2SAT you can take a variable $x$ and set it to true (or false). Then you can throw out any clauses where $x$ appears, or if a clause becomes unsatisfiable from previous assignments you know that $x$ cannot be true (or false). By proceeding in this manner we can efficiently obtain a satisfying formula or verify that the clauses are not all simultaneously satisfiable.

If you try to extend this intuition to 3SAT and set the truth value of $x$ then you will end up still having to check an exponential number of clauses before shrinking the problem size. This doesn't show that 3SAT is not polynomial-time solvable but it does show that the obvious approach for solving 2SAT fails when extended to 3SAT.

Answer 2

An algorithm running in time $2^n$ is extremely slow. Fortunately, there are better algorithms for solving 2SAT. Here is one such algorithm.

Suppose that $C_1$ and $C_2$ are two clauses (disjunctions of variables) such that $C_1$ contains some variable $x$ and $C_2$ contains its negation $\bar{x}$. Let $C$ be the clause formed by taking the disjunction of all other literals appearing in $C_1$ and $C_2$. For example, if $C_1 = x \lor y$ and $C_2 = \lnot x \lor z$, then $C = y \lor z$. The clause $C$ is known as the resolvent of $C_1$ and $C_2$; we say that it is obtained by applying the Resolution rule to $C_1$ and $C_2$. The resolvent satisfies the following property:

If $C_1$ and $C_2$ hold, then so does $C$.

Indeed, write $C_1 = x \lor \alpha$ and $C_2 = \bar{x} \lor \beta$, where $\alpha,\beta$ are clauses. In these terms, $C = \alpha \lor \beta$. Suppose that $C_1$ and $C_2$ hold. If $x$ is true then $\beta$ holds, and if $x$ is false then $\alpha$ holds. In both cases, $C$ holds.

Consequently:

If a set $\mathcal{C}$ of clauses is satisfiable and $C$ is the resolvent of $C_1,C_2 \in \mathcal{C}$, then the set $\mathcal{C} \cup \{C\}$ is also satisfiable.

For example, the CNF $(x \lor y) \land (\lnot x \lor z)$ is satisfiable, hence so is the CNF $(x \lor y) \land (\lnot x \lor z) \land (y \lor z)$.

The clauses $\alpha,\beta$ in the definition of the Resolution rule could be empty. If both are empty, then the resolvent is the empty clause, which is unsatisfiable. If we reach the empty clause after several applications of the Resolution rule, then we know that the original CNF was unsatisfiable. Conversely, it turns out that if the empty clause cannot be generated from a given CNF, then the CNF is satisfiable. This suggests the following algorithm, which gets as input a CNF in the form of a set of clauses $\mathcal{C}$:

While there exist two clauses $C_1,C_2 \in \mathcal{C}$ which can be resolved and their resolvent doesn't already belong to $\mathcal{C}$, add their resolvent to $\mathcal{C}$. If the empty clause is eventually reached, output unsatisfiable. Else, output satisfiable.

For example, the CNF $(x \lor y) \land (\lnot x \lor z)$ is satisfiable, since after adding the resolvent $(y \lor z)$ there are no new clauses which can be generated. Conversely, if we start with the CNF $(x \lor y) \land (\lnot x \lor y) \land (z \lor \lnot y) \land (\lnot z \lor \lnot y)$, then we can resolve the first two clauses to get $y$, the other two clauses to get $\lnot y$, and then the two new clauses to get the empty clause; hence the CNF is unsatisfiable.

When applying this algorithm to a 2CNF, the clauses generated always have width at most 2 (that is, they are disjunctions of at most two literals). Since there are $O(n^2)$ many such clauses, where $n$ is the number of variables, the algorithm above stops within $O(n^2)$ iterations, and consequently, it runs in polynomial time.

This is no longer the case for 3CNFs — the width can increase. For example, the resolvent of $x \lor y \lor z$ and $\lnot x \lor u \lor v$ is $y \lor z \lor u \lor v$, whose width is 4. Intuitively, this is why the Resolution algorithm is not efficient for 3CNFs. Indeed, we can exhibit examples of unsatisfiable 3CNFs in which not matter how the algorithm is applied — no matter which two clauses are resolved in each step — it takes exponentially many steps to reach the empty clause. This result is part of an area known as proof complexity.

Answer 3

2SAT is NL-complete, so 2SAT is in P. 3SAT is NP-complete, so 3SAT is not in P assuming that P unequals NP.