Classification of minimally unsatisfiable 2-CNFs

We consider minimally unsatisfiable 2-CNFs, i.e., minimally unsatisfiable conjunctive normal forms, where each clause contains at most 2 literals (short 2-MUs). Characterisations of 2-MUs in the literature have been restricted to the nonsingular case (where every variable occurs positively and negatively at least twice), and those with a unit-clause. We provide the full classification of 2-MUs, and obtain polytime isomorphism decision. The main tool used here is the implication digraph, which allows to reduce the problem of determining the isomorphism types of 2-MUs to the isomorphism types of "weak double cycles" (WDCs), obtained from the digraph versions of undirected cycles by splitting vertices and arcs. We show that these digraphs have at most one skew-symmetry, and thus the skew-symmetric WDCs can be considered as 2-CNFs.