  We consider minimally unsatisfiable 2-CNFs (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 F. The main tool is
the implication digraph, and we show that the implication digraph of F is a
"weak double cycle" (WDC), a big cycle of small cycles (with possible
overlaps). Combining logical and graph-theoretical methods, we prove that WDCs
have at most one skew-symmetry, and thus we obtain that the isomorphisms
between 2-MUs F, F' are exactly the isomorphisms between their implication
digraphs.
  We obtain a variety of applications. For fixed deficiency k, the difference
of the number of clauses of F and the number n of variables of F, the
automorphism group of F is a subgroup of the Dihedral group with 4k elements.
The isomorphism problem restricted to 2-MUs F is decidable in linear time for
fixed k. The number of isomorphism types of 2-MUs for fixed k is
Theta(n^(3k-1)). The smoothing (removal of linear vertices) of skew-symmetric
WDCs corresponds exactly to the canonical normal form of F obtained by
1-singular DP-reduction, a restricted form of DP-reduction (or "variable
elimination") only reducing variables of degree 2. The isomorphism types of
these normal forms, i.e., the homeomorphism types of skew-symmetric WDCs, are
in one-to-one correspondence with binary bracelets (or "turnover necklaces") of
length k.
