Computing Unsatisfiable k-SAT Instances with Few Occurrences per VariableTheoretical Computer Science, vol. 337, no. 1-3, pp. 347-359, 2005. Download: [paper ps] [paper pdf] [supplementary material] Abstract:(k,s)-SAT is the propositional satisfiability problem restricted to instances where each clause has exactly k distinct literals and every variable occurs at most s times. It is known that there exists an exponential function f such that for s smaller or equal f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k>2). Exact values of f are only known for k=3 and k=4, and it is open whether f is computable.We introduce a computable function f1 which bounds f from above and determine the values of f1 by means of a calculus of integer sequences. This new approach enables us to improve the best known upper bounds for f(k), generalizing the known constructions for unsatisfiable (k,s)-SAT instances for small k. [back to Stefan Szeider's homepage] |