I don't quite understand why the resolution algorithm completes in polynomial time for 2SAT but not 3SAT.

I'm looking at slide 42 of these slides for reference. It is clear that given two clauses of length at most 2, their resolvent has length at most 2. From $k$ propositional variables $x_1,\dots,x_k$, I see that there are $(2k)^2=4k^2$ possible clauses of the form $(a\lor b)$ where $a,b\in\{x_i\}\cup\{\lnot{x_i}\}$, so there are $O(k^2)$ possible clauses of length at most 2.

But how is this used to show that the resolution algorithm runs in polynomial time for 2SAT but not 3SAT?


In the case of 2SAT, resolving two clauses does not increase their width (the width of a clause is the number of literals appearing in it). This is not the case for 3SAT, where resolution could increase the width. For example, if we resolve $a \lor b \lor c$ and $\lnot a \lor d \lor e$, both of width 3, we get the clause $b \lor c \lor d \lor e$ of width 4.

When running resolution on an instance of 2SAT on $n$ variables, we necessarily get stuck after at most $4n^2 + 2n + 1$ steps, since this is the total number of clauses that we could encounter. This shows that resolution runs in polynomial time on 2SAT.

Showing that resolution does not run in polynomial time on 3SAT is much more involved, among else since resolution is not really an algorithm but rather a proof system. Perhaps the simplest proof can be found in Ben-Sasson and Wigderson's classic paper Short proofs are narrow – Resolution made simple.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.