On the size of minimal unsatisfiable formulas (Q1010894)

Summary: 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 \textit{L. Lovász} [Stud. Sci. Math. Hung. 11, 113--114 (1976; Zbl 0425.05026)] which asserts that a critically 3-chromatic \(k\)-uniform hypergraph can have at most \(\binom {n}{k-1}\) edges.