A Note on Unsatisfiable k -CNF Formulas with Few Occurrences per Variable
Shlomo Hoory, Stefan Szeider · SIAM Journal on Discrete Mathematics · 2006
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 \leq f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k \geq 3). We prove that f(k) = O(2 k \cdot log k/k), improving upon the best known upper bound O(2 k /k alpha ), where alpha=log 3 4 - 1 \approx 0.26. The new upper bound is tight up to a log k factor with the best known lower bound Omega(2 k /k).