Sign up ×
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|cite|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

3 Answers 3

up vote 1 down vote accepted

Your statement is not true because you only counted the clauses containing 3 & 2 & 1 literals but some times two clause of size 3 can produce a clause of size 4 and also two clause of size 4 can led to a resolvent clause of size 6. Thus there is not a well-known bound on the number of clauses that may produce.

share|cite|improve this answer
Thank you for your answer. That was my mistake, thank you. – John Threepwood Apr 29 at 16:54

Using some algorithms like DPLL or CDCL SAT solvers leads to much less than $2^n$ candidate testing but still an exponential function.

Also, in local search algorithms best bounds are about $1.333^n$ by Schöning's 1999 paper.

share|cite|improve this answer
This question is very old and already has good answers. It is probably better to spend your effort to write very good answers for unanswered questions. I personally do not see what this contributes to the answers already provided. – TravisJ Sep 19 at 16:44

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