A note on unsatisfiable k-CNF formulas with few occurrences per variableSIAM Journal on Discrete Mathematics, vol. 20, no. 2, pp. 523—528, 2006. Download: [paper ps] [paper pdf] Abstract:(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 less or equal f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k>2). 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 log k/k), which is tight up to a log k factor.[back to Stefan Szeider's homepage] |