# How many clauses are required for SAT to be NP-hard in CNF formulas?

It is not hard to see that SAT for a CNF formula with $$n$$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $$n$$ variables and $$O(n)$$ clauses is enough for NP-hardness (consider for example the instances of SAT associated with the natural formula for 3-colorability, applied to planar graphs).

We could define this formally as $$\text{CNFSAT}-f-\text{Clauses}$$, a family of problems parameterized by a function $$f$$, in which instances are formulas in CNF such that if they have $$n$$ variables, then they have at most $$f(n)$$ clauses. Based on this, what I’d like to know is what is the smallest function $$g$$ such that we know there exists $$f \in O(g)$$ such that $$\text{CNFSAT}-f-\text{Clauses}$$ is already NP-hard. We know that g = 1 (constant # of clauses) does not work, and $$g = n$$ (linear number of clauses) works.

What about $$g = \log n$$? Is there a simple algorithm for CNFSAT over formulas that have $$O(\lg \lg n)$$ clauses?