On the size of minimal unsatisfiable formulas

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 $\mathrm{\Omega }(n^k)$ clauses for $k\ge 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 $\left(\genfrac{}{}{0px}{}{n}{k-1}\right)$ edges.