# Showing resolution algorithm for 2SAT is polynomial time

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?

## 1 Answer

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.