Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

A SAT instance in CNF with $n$ variables has at most $2^n$ resolvents, therefore the resolution method is not in polynomial time.

Considering a 3-SAT instance, we have at most $n^3 + n^2 + n$ many resolvents. Therefore, we can decide 3-SAT in polynomial time by resolution.

I am sure, my second statement is wrong, because otherwise we would have $P = NP$. But I can not see my mistake. Can someone bring clarification here?

share|improve this question
Your second statement is wrong, but I don't see how we can explain your mistake if you don't explain how you arrived at it. –  Eric Tressler Jul 4 '13 at 12:42
@EricTressler Roughly: All 1-Literal clauses: $n$ many. All 2-Literal clauses $n^2$ many. All 3-Literal clauses $n^3$ many. Calculate all clauses (polynomial many) and check for an empty clause. –  John Threepwood Jul 4 '13 at 12:49
The problem is that to determine if a CNF instance is satisfiable, you have to assign boolean values to each of the variables $x_i$ so that all of the existing clauses are satisfied simultaneously. You can't deal with them one by one, so you still have $2^n$ possible assignments of the $x_i$. –  Eric Tressler Jul 4 '13 at 13:38
@EricTressler Thank you for the reply. Resolution is refutation complete: A SAT instance is satisfiable iff the empty clause can not be derived as resolvent. So building all resolvents is sufficient to test for satisfiability. –  John Threepwood Jul 4 '13 at 13:50

1 Answer 1

There are only that many clauses but that only gives an upper bound for the time to test a single candidate solution. There are still $2^n$ candidates to test.

share|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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