A note on unsatisfiable k-CNF formulas with few occurrences per variable

The ( k, s)-SAT problem is the satisfiability problem restricted to instances where each clause has exactly k literals and every variable occurs at most s times. It is known that there exists a function f such that for s <= f( k) all ( k, s)-SAT instances are satisfiable, but ( k, f( k)+ 1)- SAT is already NP-complete ( k >= 3). We prove that f( k) = O(2(k) . log k/k), improving upon the best known upper bound O(2(k)/k(alpha)), where alpha = log(3) 4 - 1 approximate to 0.26. The new upper bound is tight up to a log k factor with the best known lower bound Omega(2(k)/k).