ABSTRACT. Minimally Unsatisfiable clause-sets (MUs) are building blocks for understanding Minimally Unsatisfiable Sub-clause-sets (MUSs), and they are also interesting in their own right, as hardest unsatisfiable clause-sets. There are two important previously known but isolated characterisations for MUs, 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. We obtain unique isomorpism type descriptions of normal forms, for both cases.

An MSD is a strongly connected digraph, where removing any arc destroys the strong connectedness. We introduce the new class DFM of special MUs, which are in close correspondence to MSDs. The known relation between 2-CNFs and digraphs is used, but in a simpler and more direct way. The non-binary clauses in DFMs can be ignored. For a binary clause (a or b) normally both arcs (-a -> b) and (-b -> a) need to be considered, but here we have a canonical choice of one of them.

The definition of DFM is indeed very simple: an MU, where all clauses except of two are binary, while the two non-binary clauses are the two "full monotone clauses", the disjunction of all variables and the disjunction of all negated variables. We expect this basic class of MUs to be very useful in the future. Every variables occurs at least twice positively and twice negatively ("non-singularity"), and its isomorphism problem is GI-complete, while we have polytime decision, and likely we have good properties related to MUS-search. Via "saturations" and "marginalisations", adding resp. removing literal occurrences, as well as via "non-singular extensions", adding new variables, this class reaches out to apparently unrelated classes.