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?