On the size of minimal unsatisfiable formulas

TL;DR

This paper constructs large minimal unsatisfiable formulas in k-SAT, showing they can have significantly more clauses than previously known, thus answering a longstanding open question.

Contribution

It provides the first construction of minimal unsatisfiable k-SAT formulas with (n^k) clauses for all k , advancing understanding of their size.

Findings

Minimal unsatisfiable k-SAT formulas can have (n^k) clauses for k 

Negatively answers Rosenfeld's question about clause bounds

Comparison with Lovász's hypergraph result highlights the formulas' large size

Abstract

An unsatisfiable formula is called minimal if it becomes satisfiable whenever any of its clauses are removed. We construct minimal unsatisfiable $k$-SAT formulas with $\Omega(n^k)$ clauses for $k \geq 3$, thereby negatively answering a question of Rosenfeld. This should be compared to the result of Lov\'asz which asserts that a critically 3-chromatic $k$-uniform hypergraph can have at most $\binom{n}{k-1}$ edges.