Minimal Unsatisfiability and Minimal Strongly Connected Digraphs

Minimally unsatisfiable clause-sets (MUs) are the hardest unsatisfiable clause-sets. There are two important but isolated characterisations for nonsingular MUs (every literal occurs at least twice), both with ingenious but complicated proofs: Characterising 2-CNF MUs, and characterising MUs with deficiency 2 (two more clauses than variables). Via a novel connection to Minimal Strong Digraphs (MSDs), we give short and intuitive new proofs of these characterisations, revealing an underlying common structure.