Small unsatisfiable $k$-CNFs with bounded literal occurrence

Tianwei Zhang, Tomáš Peitl, Stefan Szeider

We obtain the smallest unsatisfiable formulas in subclasses of $k$-CNF (exactly $k$ distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiabl…