Families of unsatisfiable k-CNF formulas with few occurrences per variable
(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\leq f (k) all (k, s)-SAT instances are satisfiable, but (k, f (k)+ 1)-SAT is already
NP-complete (k\geq 3). The best known lower and upper bounds on f (k) are Omega (2^ k/k)
and O (2^ k/k^ a), where a=\log_3 4-1= 0.26.... We prove that f (k)= O (2^ k\cdot\log k/k),
which is tight up to a\log k factor.
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). The best known lower and upper bounds on f (k) are Omega (2^ k/k)
and O (2^ k/k^ a), where a=\log_3 4-1= 0.26.... We prove that f (k)= O (2^ k\cdot\log k/k),
which is tight up to a\log k factor.
(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\leq f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k\geq 3). The best known lower and upper bounds on f(k) are Omega(2^k/k) and O(2^k/k^a), where a=\log_3 4 - 1 = 0.26.... We prove that f(k) = O(2^k \cdot \log k/k), which is tight up to a \log k factor.
arxiv.org