SAT 2004 START ConferenceManager    


Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable

Shlomoh Hoory, Stefan Szeider

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


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 [Kratochvil, Savicky, Tuza 93] that there exists an exponential function f such that if s does not exceed 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.

Based on techniques of [Davydov, Davydova, Kleine Buning 98], we introduce a computable function f1 which bounds f from above. We develop a calculus of integer sequences to determine the values of f1. 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 [Tovey 84; Dubois 90; Stribrna 94; Berman, Karpinski, Scott 03].


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com