Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
Boolean Satisfiability (CNF-SAT) problem in $n$ variables may contain a CNF formula with $O(2^n)$ clauses in the worst case.
My question is: Wouldn't a program reading a CNF formula have to asymptotically run $O(2^n)$ steps? Is the search for a sub-exponential CNF-SAT algorithm moot?
No. The meaning of "polynomial-time" is "polynomial in the length of an input". We can still search for an algorithm that is efficient on short inputs.
For instance, suppose we have CNF formulas with $n$ variables and only $10n$ clauses. No one knows how to solve this in time polynomial in $n$.
