Families of unsatisfiable k-CNF formulas with few occurrences per variable

Original · EN

(k,s)-SAT 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). The best known lower and upper bounds on f(k) are Omega(2ᵏ/k) and O(2ᵏ/kᵃ), where a=₃ 4 - 1 = 0.26.... We prove that f(k) = O(2ᵏ · k/k), which is tight up to a k factor.