Computing unsatisfiable k-SAT instances with few occurrences per variable

(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⩽f(k) all (k,s)-SAT instances are satisfiable, but (k,f(k)+1)-SAT is already NP-complete (k⩾3). Exact values of f are only known for k=3 and 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.