Families of unsatisfiable k-CNF formulas with few occurrences per variable

Shlomo Hoory, Stefan Szeider

(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…