The classification of minimally unsatisfiable 2-CNFs -- a fundamental study

Hoda Abbasizanjani; Oliver Kullmann

arxiv: 2003.03639 · v3 · submitted 2020-03-07 · 💻 cs.DM · math.CO

The classification of minimally unsatisfiable 2-CNFs -- a fundamental study

Hoda Abbasizanjani , Oliver Kullmann This is my paper

Pith reviewed 2026-05-24 14:49 UTC · model grok-4.3

classification 💻 cs.DM math.CO

keywords minimally unsatisfiable 2-CNFimplication digraphweak double cycleskew-symmetrydeficiencyisomorphism classificationDavis-Putnam reductionbinary bracelets

0 comments

The pith

Minimally unsatisfiable 2-CNFs are classified up to isomorphism because their implication digraphs are weak double cycles admitting at most one skew-symmetry.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper classifies all minimally unsatisfiable 2-CNF formulas up to isomorphism. It proves that the implication digraph of any such formula must be a weak double cycle, formed as a large cycle built from smaller cycles that may overlap. These digraphs are shown to possess at most one skew-symmetry, defined as a self-inverse fixed-point-free anti-automorphism that reverses all arc directions. The single possible skew-symmetry implies that two formulas are isomorphic precisely when their implication digraphs are isomorphic. This reduction supplies immediate corollaries for formulas of fixed deficiency, including quadratic-time isomorphism testing and an asymptotic count of Theta(n to the power 3k minus 1).

Core claim

The implication digraph of any minimally unsatisfiable 2-CNF is a weak double cycle. Weak double cycles admit at most one skew-symmetry. Consequently the isomorphisms between two minimally unsatisfiable 2-CNFs are exactly the isomorphisms between their implication digraphs, reducing the entire classification problem to the classification of this structured class of digraphs.

What carries the argument

The weak double cycle in the implication digraph, equipped with its at most one skew-symmetry, which equates logical isomorphism of the formulas with ordinary digraph isomorphism.

If this is right

For deficiency k the smoothing operation on skew-symmetric weak double cycles produces exactly the canonical normal form obtained by one-singular Davis-Putnam reduction.
The homeomorphism types of these weak double cycles stand in one-to-one correspondence with binary bracelets of length k.
The automorphism group of any minimally unsatisfiable 2-CNF of deficiency k is a subgroup of the dihedral group of order 4k.
The isomorphism problem for minimally unsatisfiable 2-CNFs is decidable in quadratic time.
The number of isomorphism types of minimally unsatisfiable 2-CNFs of fixed deficiency k is Theta(n to the power 3k minus 1).

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Enumeration of binary bracelets immediately yields an enumeration procedure for all minimally unsatisfiable 2-CNFs of each fixed deficiency.
The quadratic-time isomorphism test supplies a practical algorithm for deciding logical equivalence of small 2-CNF instances arising in verification or constraint problems.
The structural restriction to weak double cycles may serve as a template for attempting analogous reductions in minimally unsatisfiable formulas whose clauses have length greater than two.

Load-bearing premise

The implication digraph of every minimally unsatisfiable 2-CNF is necessarily a weak double cycle whose only possible non-trivial automorphism is a single skew-symmetry.

What would settle it

Exhibition of one minimally unsatisfiable 2-CNF whose implication digraph is not a weak double cycle, or of one weak double cycle that possesses two distinct skew-symmetries.

read the original abstract

Conjunctive normal forms where every clause has length at most two are called 2-CNFs. We study minimally unsatisfiable 2-CNFs (2-MUs), that is, unsatisfiable 2-CNFs where removing any clause destroys unsatisfiability, and obtain their full classification up to isomorphism. The main tool is the implication digraph: we show that for 2-MUs these digraphs are "weak double cycles" (WDCs), big cycles of small cycles with possible overlaps. Combining logical and graph-theoretical methods, we prove that WDCs have at most one skew-symmetry (a self-inverse fixed-point-free anti-automorphism reversing the direction of arcs). It follows that the isomorphisms between 2-MUs are exactly the isomorphisms between their implication digraphs, reducing the classification of 2-MUs to the classification of a well-structured class of digraphs. We obtain a variety of applications for 2-MUs of deficiency k (the difference between the number of clauses and the number of variables): the smoothing of skew-symmetric WDCs corresponds exactly to the canonical normal form obtained by 1-singular Davis-Putnam reduction, and the resulting homeomorphism types are in one-to-one correspondence with binary bracelets of length k. The automorphism group of any 2-MU of deficiency k is a subgroup of the dihedral group with 4k elements. The isomorphism problem for 2-MUs is decidable in quadratic time, and the number of isomorphism types of 2-MUs for fixed k is Theta(n^(3k-1)). The article is addressed to both the logic and the graph theory communities, with complete proofs provided throughout.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper classifies all minimally unsatisfiable 2-CNFs up to isomorphism by proving their implication digraphs are weak double cycles with at most one skew-symmetry, plus a bracelet bijection and quadratic isomorphism test.

read the letter

The core result is a full isomorphism classification of 2-MUs. The authors show that the implication digraph of any such formula is a weak double cycle, prove these digraphs admit at most one skew-symmetry, and conclude that formula isomorphisms match digraph isomorphisms. From there they get an explicit correspondence between the homeomorphism types for fixed deficiency k and binary bracelets, plus the automorphism group bound inside the dihedral group of order 4k, quadratic-time isomorphism, and the Theta(n^{3k-1}) count of types. These pieces are presented as new and rest on direct graph-theoretic and logical arguments rather than reductions of prior theorems. The paper does the work of spelling out the constructions, the uniqueness proof, and the algorithmic consequences in one place, with complete proofs supplied. That combination of a structural characterization with concrete enumeration and complexity payoffs is the useful part. The scope stays inside 2-CNF minimality, so the results do not reach beyond that corner of satisfiability or digraph theory; that is not a flaw but it does limit the audience. The central WDC claim and the single-skew-symmetry bound are the load-bearing steps, and the abstract states they are proved explicitly with no indicated gaps. No internal contradictions or post-hoc choices appear in the argument outline. This is for people already working on minimal unsatisfiability, implication graphs, or exact enumeration in SAT. A reader who needs the classification, the bracelet link, or the complexity statements will find them here. It is worth sending to peer review because the new structural objects and the verifiable consequences are substantial enough to merit referee attention even if revisions are needed on the cycle-overlap cases.

Referee Report

0 major / 2 minor

Summary. The paper provides the full classification of minimally unsatisfiable 2-CNFs (2-MUs) up to isomorphism. Using implication digraphs, it shows that for 2-MUs these are weak double cycles (WDCs). It proves that WDCs have at most one skew-symmetry, implying that isomorphisms between 2-MUs are exactly the isomorphisms between their implication digraphs. This reduces the classification to that of WDCs. Applications for deficiency k include correspondence of smoothing of skew-symmetric WDCs to canonical normal forms via 1-singular Davis-Putnam reduction, homeomorphism types corresponding to binary bracelets of length k, automorphism groups as subgroups of the dihedral group of order 4k, quadratic time decidability of isomorphism, and Theta(n^(3k-1)) number of isomorphism types.

Significance. If the central claims hold, the paper delivers a complete structural classification of 2-MUs, with explicit graph-theoretic characterization and logical implications. The combination of methods, the proof of the skew-symmetry bound, and the resulting applications to normal forms, automorphism groups, and computational complexity represent a significant advance for the study of minimally unsatisfiable formulas. The provision of complete proofs throughout is a strength.

minor comments (2)

Abstract: the informal description of WDCs as 'big cycles of small cycles with possible overlaps' would benefit from an immediate parenthetical reference to the formal definition given later in the paper.
Abstract: the quadratic-time claim for the isomorphism problem would be strengthened by specifying the input measure (e.g., total number of literals or clauses).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive and detailed summary of our paper, the assessment of its significance, and the recommendation to accept. We are pleased that the central claims and contributions were found to be of interest to both the logic and graph theory communities.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper introduces the standard implication digraph for 2-CNFs and explicitly defines the new WDC class, then supplies direct proofs combining logical and graph-theoretic arguments to establish that every 2-MU implication digraph is a WDC and that WDCs admit at most one skew-symmetry. These proofs are presented as self-contained within the manuscript, with no reduction of any central claim to a fitted parameter, a self-referential definition, or a load-bearing self-citation whose content is merely renamed. The subsequent reduction of 2-MU isomorphisms to digraph isomorphisms, the automorphism bounds, and the complexity results all follow from the stated independent arguments rather than from any circular re-use of inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claims rest on the newly introduced definition of weak double cycles and the standard implication-digraph construction; no numerical free parameters appear, and the only invented entity is the WDC itself.

axioms (1)

standard math The implication digraph of a 2-CNF is constructed by placing a directed arc from each literal to the negation of the other literal in every clause.
Standard construction used throughout 2-SAT literature and invoked without proof in the abstract.

invented entities (1)

weak double cycle (WDC) no independent evidence
purpose: To capture exactly the digraphs arising from minimally unsatisfiable 2-CNFs
Newly defined in the paper as big cycles of small cycles with possible overlaps; no independent falsifiable prediction outside the classification is supplied.

pith-pipeline@v0.9.0 · 5849 in / 1434 out tokens · 36814 ms · 2026-05-24T14:49:49.808087+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages

[1]

Minimal unsatisﬁability and minimal strongly connected digraphs

Hoda Abbasizanjani and Oliver Kullmann. Minimal unsatisﬁability and minimal strongly connected digraphs. In Olaf Beyersdorﬀ and Chris toph M. Wintersteiger, editors, Theory and Applications of Satisﬁability Testing - SAT 2018, volume 10929 of Lecture Notes in Computer Science , pages 329–

work page 2018
[2]

doi:10.1007/978-3-319-94144-8_20

Springer, 2018. doi:10.1007/978-3-319-94144-8_20

work page doi:10.1007/978-3-319-94144-8_20 2018
[3]

Minimal non-two-colorable hyperg raphs and minimal unsatisﬁable formulas

Ron Aharoni and Nathan Linial. Minimal non-two-colorable hyperg raphs and minimal unsatisﬁable formulas. Journal of Combinatorial Theory, Series A , 43(2):196–204, November 1986. doi:10.1016/0097-3165(86) 90060-9. 16

work page doi:10.1016/0097-3165(86 1986
[4]

Plass, and Robert Endre Tarjan

Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linea r- time algorithm for testing the truth of certain quantiﬁed boolean fo r- mulas. Information Processing Letters , 8(3):121–123, March 1979. doi: 10.1016/0020-0190(79)90002-4

work page doi:10.1016/0020-0190(79)90002-4 1979
[5]

Subramani

Hans Kleine B¨ uning, Piotr Wojciechowski, and K. Subramani. On th e com- putational complexity of read once resolution decidability in 2CNF for mu- las. In T. Gopal, G. Jger, and S. Steila, editors, International Conference on Theory and Applications of Models of Computation (TAMC 20 17), vol- ume 10185 of Lecture Notes in Computer Science (LNCS) , pages...

work page doi:10.1007/978-3-319-55911-7_26 2017
[6]

Minimum witnesses fo r unsatisﬁable 2CNFs

Joshua Buresh-Oppenheim and David Mitchell. Minimum witnesses fo r unsatisﬁable 2CNFs. In Armin Biere and Carla P. Gomes, editors, The- ory and Applications of Satisﬁability Testing - SAT 2006 , volume 4121 of Lecture Notes in Computer Science , pages 42–47. Springer, 2006. doi: 10.1007/11814948_6

work page doi:10.1007/11814948_6 2006
[7]

Chv´ atal and Bruce Reed

V. Chv´ atal and Bruce Reed. Mick gets some (the odds are on his side). In Proc. 33th Annual Symposium on Foundations of Computer Scie nce (Pittsburgh, PA) , pages 620–627. IEEE Comput. Soc. Press, 1992. doi: 10.1109/SFCS.1992.267789

work page doi:10.1109/sfcs.1992.267789 1992
[8]

Yves Crama and Peter L. Hammer. Boolean Functions: Theory, Algo- rithms, and Applications , volume 142 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2011. ISBN 978-0-521-84751- 3

work page 2011
[9]

An e ﬃcient algorithm for the minimal unsatisﬁability problem for a subclass of CNF

Gennady Davydov, Inna Davydova, and Hans Kleine B¨ uning. An e ﬃcient algorithm for the minimal unsatisﬁability problem for a subclass of CNF . Annals of Mathematics and Artiﬁcial Intelligence , 23(3-4):229–245, 1998. doi:10.1023/A:1018924526592

work page doi:10.1023/a:1018924526592 1998
[10]

Fernandez de La Vega

W. Fernandez de La Vega. Random 2-SAT: results and problems. Theoret- ical Computer Science , 265:131–146, 2001. doi:10.1016/S0304-3975(01) 00156-6

work page doi:10.1016/s0304-3975(01 2001
[11]

Gilbert and John Riordan

E.N. Gilbert and John Riordan. Symmetry types of periodic seque nces. Illinois Journal of Mathematics , 5(4):657–665, 1961. doi:10.1215/ijm/ 1255631587

work page doi:10.1215/ijm/ 1961
[12]

Goldberg and Alexander V

Andrew V. Goldberg and Alexander V. Karzanov. Path problems in skew-symmetric graphs. Combinatorica, 16:353–382, 1996. doi:10.1007/ BF01261321

work page 1996
[13]

Gross and Jay Yellen, editors

Jonathan L. Gross and Jay Yellen, editors. Handbook of Graph Theory . Discrete Mathematics and Its Applications. CRC Press, 2003. ISBN 1- 58488-090-2; QA166.H36

work page 2003
[14]

Vaibhav Karve and Anil N. Hirani. The complete set of minimal simple graphs that support unsatisﬁable 2-CNFs. Discrete Applied Mathematics ,

work page
[15]

doi:10.1016/j.dam.2019.12.017

In press. doi:10.1016/j.dam.2019.12.017. 17

work page doi:10.1016/j.dam.2019.12.017 2019
[16]

On subclasses of minimal unsatisﬁable formu - las

Hans Kleine B¨ uning. On subclasses of minimal unsatisﬁable formu - las. Discrete Applied Mathematics , 107(1-3):83–98, 2000. doi:10.1016/ S0166-218X(00)00245-6

work page 2000
[17]

Minimal unsatisﬁability and autarkies

Hans Kleine B¨ uning and Oliver Kullmann. Minimal unsatisﬁability and autarkies. In Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisﬁability , volume 185 of Frontiers in Artiﬁcial Intelligence and Applications , chapter 11, pages 339–401. IOS Press, February 2009. doi:10.3233/978-1-58603-929-5-339

work page doi:10.3233/978-1-58603-929-5-339 2009
[18]

The complexity of homomorph isms and renamings for minimal unsatisﬁable formulas

Hans Kleine B¨ uning and Daoyun Xu. The complexity of homomorph isms and renamings for minimal unsatisﬁable formulas. Annals of Mathe- matics and Artiﬁcial Intelligence , 43(1-4):113–127, 2005. doi:10.1007/ s10472-005-0422-8

work page 2005
[19]

Minimal unsatisﬁability: Re- sults and open questions

Hans Kleine B¨ uning and Xishun Zhao. Minimal unsatisﬁability: Re- sults and open questions. Technical Report tr-ri-02-230, Series Com- puter Science, University of Paderborn, University of Paderborn , De- partment of Mathematics and Computer Science, 2002. http://wwwcs. uni-paderborn.de/cs/ag-klbue/de/research/MinUnsat/i ndex.html

work page 2002
[20]

An application of matroid theory to the SAT prob- lem

Oliver Kullmann. An application of matroid theory to the SAT prob- lem. In Proceedings of the 15th Annual IEEE Conference on Computa- tional Complexity , pages 116–124, July 2000. See also TR00-018, Elec- tronic Colloquium on Computational Complexity (ECCC), March 2000. doi:10.1109/CCC.2000.856741

work page doi:10.1109/ccc.2000.856741 2000
[21]

On Davis-Putnam reductions for min- imally unsatisﬁable clause-sets

Oliver Kullmann and Xishun Zhao. On Davis-Putnam reductions for min- imally unsatisﬁable clause-sets. Theoretical Computer Science , 492:70–87, June 2013. doi:10.1016/j.tcs.2013.04.020

work page doi:10.1016/j.tcs.2013.04.020 2013
[22]

Redundancy in logic II: 2CNF and Horn propos itional formulae

Paolo Liberatore. Redundancy in logic II: 2CNF and Horn propos itional formulae. Artiﬁcial Intelligence , 172(2-3):265–299, February 2008. doi: 10.1016/j.artint.2007.06.003

work page doi:10.1016/j.artint.2007.06.003 2008
[23]

Eugene M. Luks. Isomorphism of graphs of bounded valence ca n be tested in polynomial time. Journal of Computer and System Sciences , 25(1):42– 65, August 1982. doi:10.1016/0022-0000(82)90009-5

work page doi:10.1016/0022-0000(82)90009-5 1982
[24]

Characterization of e ven directed graphs

Paul Seymour and Carsten Thomassen. Characterization of e ven directed graphs. Journal of Combinatorial Theory Series B , 42(1):36–45, 1987. doi: 10.1016/0095-8956(87)90061-X

work page doi:10.1016/0095-8956(87)90061-x 1987
[25]

Neil J.A. Sloane. The On-Line Encyclopedia of Integer Sequence s (OEIS),

work page
[26]

antipodal

Available from: http://oeis.org/. 18 A The running example The running example of the paper is based on B3, which has the following implication digraph (3 variables, thus 6 vertices, and 6 clauses, thus 2 ·6 = 12 arcs): idg(B3) = v1 →→ ↙↙ K1 v2 →→←← K2 v3 ↙↙ ←← − K3 {v1, v2}, {v1, v2}, {v2, v3}, {v2, v3}, {v1, v3}, {v1, v3} K3 v3 →→ ↗↗ − K2 v2 →→←← − K1 v...

work page
[27]

U 2 n” listed below (with “U

This yields “U 2 n” listed below (with “U” for “unit”), which makes sense for n ≥ 1, and thus covers all cases with exactly two unit-clauses. To give a n overview, we list also the other three cases now (discussed below). They all generalise just the two unit-clauses. Let M := {{− 1, 2}, . . . ,{− (n − 1), n}} for n ∈ N (and with n − 1 clauses) be the inv...

work page
[28]

U2 n := M ∪ {{ 1}, {− n}} for n ≥ 1

work page
[29]

U1 n,i := M ∪ {{ 1}, {− n, − i}} for n ≥ 2, 1 ≤ i ≤ n − 1

work page
[30]

U0 n,i := M ∪ {{ 1, i}, {− n, − i}} for n ≥ 3, 2 ≤ i ≤ n+1 2

work page
[31]

For the ﬁrst case, with two units, we have shown: Lemma C.3 For F ∈ 2–MUδ=1 holds F ∼ = U2 n(F ) iﬀ F has two unit-clauses

U0 n,x,y = M ∪ {{ 1, x}, {− n, − y}} for n ≥ 4, 2 ≤ x < y ≤ n − 1, x + y ≤ n + 1. For the ﬁrst case, with two units, we have shown: Lemma C.3 For F ∈ 2–MUδ=1 holds F ∼ = U2 n(F ) iﬀ F has two unit-clauses. 23 The implication digraph of U 2 n is a cycle digraph with 2 n vertices and 2 n edges (where all vertices have degree 2). The labelled digraph, actual...

work page
[32]

anti-automorphism

And from {− x, 3}, {− x, − 3}, renamed to {− x, p + 1 }, {− x, − (p + 1)}, we obtain {− x, p + 1}, . . . ,{− q, − x} for some q ≥ p + 1. Appending these chains yields with the original {− 1} a clause-set isomorphic to {− 1}, {1, 2}, . . . ,{− (n− 1), n}, {n, − i} for some 2 ≤ i < n and n ≥ 2. After ﬂipping literal 1, this is U 2 n, when adding to the last...

work page
[33]

For complementary unit-clauses in F , idg(F ) is the cycle digraph of length 2, while ig( F ) is the complete graph with two vertices

work page
[34]

inf” meaning “unbo unded

Equivalence-clauses {x, y}, { x, y} ∈ F yield a cycle digraph of length 2 in idg(F ), and a single edge in ig( F ). We see from the implication digraphs, that here only the ﬁrst case ha ppens, i.e., when n(F ) = 1. This is the case U 2 1, which doesn’t pose any problems. For the sequel of the proof we assume n(F ) ≥ 2, and thus no contractions happen when...

work page

[1] [1]

Minimal unsatisﬁability and minimal strongly connected digraphs

Hoda Abbasizanjani and Oliver Kullmann. Minimal unsatisﬁability and minimal strongly connected digraphs. In Olaf Beyersdorﬀ and Chris toph M. Wintersteiger, editors, Theory and Applications of Satisﬁability Testing - SAT 2018, volume 10929 of Lecture Notes in Computer Science , pages 329–

work page 2018

[2] [2]

doi:10.1007/978-3-319-94144-8_20

Springer, 2018. doi:10.1007/978-3-319-94144-8_20

work page doi:10.1007/978-3-319-94144-8_20 2018

[3] [3]

Minimal non-two-colorable hyperg raphs and minimal unsatisﬁable formulas

Ron Aharoni and Nathan Linial. Minimal non-two-colorable hyperg raphs and minimal unsatisﬁable formulas. Journal of Combinatorial Theory, Series A , 43(2):196–204, November 1986. doi:10.1016/0097-3165(86) 90060-9. 16

work page doi:10.1016/0097-3165(86 1986

[4] [4]

Plass, and Robert Endre Tarjan

Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan. A linea r- time algorithm for testing the truth of certain quantiﬁed boolean fo r- mulas. Information Processing Letters , 8(3):121–123, March 1979. doi: 10.1016/0020-0190(79)90002-4

work page doi:10.1016/0020-0190(79)90002-4 1979

[5] [5]

Subramani

Hans Kleine B¨ uning, Piotr Wojciechowski, and K. Subramani. On th e com- putational complexity of read once resolution decidability in 2CNF for mu- las. In T. Gopal, G. Jger, and S. Steila, editors, International Conference on Theory and Applications of Models of Computation (TAMC 20 17), vol- ume 10185 of Lecture Notes in Computer Science (LNCS) , pages...

work page doi:10.1007/978-3-319-55911-7_26 2017

[6] [6]

Minimum witnesses fo r unsatisﬁable 2CNFs

Joshua Buresh-Oppenheim and David Mitchell. Minimum witnesses fo r unsatisﬁable 2CNFs. In Armin Biere and Carla P. Gomes, editors, The- ory and Applications of Satisﬁability Testing - SAT 2006 , volume 4121 of Lecture Notes in Computer Science , pages 42–47. Springer, 2006. doi: 10.1007/11814948_6

work page doi:10.1007/11814948_6 2006

[7] [7]

Chv´ atal and Bruce Reed

V. Chv´ atal and Bruce Reed. Mick gets some (the odds are on his side). In Proc. 33th Annual Symposium on Foundations of Computer Scie nce (Pittsburgh, PA) , pages 620–627. IEEE Comput. Soc. Press, 1992. doi: 10.1109/SFCS.1992.267789

work page doi:10.1109/sfcs.1992.267789 1992

[8] [8]

Yves Crama and Peter L. Hammer. Boolean Functions: Theory, Algo- rithms, and Applications , volume 142 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2011. ISBN 978-0-521-84751- 3

work page 2011

[9] [9]

An e ﬃcient algorithm for the minimal unsatisﬁability problem for a subclass of CNF

Gennady Davydov, Inna Davydova, and Hans Kleine B¨ uning. An e ﬃcient algorithm for the minimal unsatisﬁability problem for a subclass of CNF . Annals of Mathematics and Artiﬁcial Intelligence , 23(3-4):229–245, 1998. doi:10.1023/A:1018924526592

work page doi:10.1023/a:1018924526592 1998

[10] [10]

Fernandez de La Vega

W. Fernandez de La Vega. Random 2-SAT: results and problems. Theoret- ical Computer Science , 265:131–146, 2001. doi:10.1016/S0304-3975(01) 00156-6

work page doi:10.1016/s0304-3975(01 2001

[11] [11]

Gilbert and John Riordan

E.N. Gilbert and John Riordan. Symmetry types of periodic seque nces. Illinois Journal of Mathematics , 5(4):657–665, 1961. doi:10.1215/ijm/ 1255631587

work page doi:10.1215/ijm/ 1961

[12] [12]

Goldberg and Alexander V

Andrew V. Goldberg and Alexander V. Karzanov. Path problems in skew-symmetric graphs. Combinatorica, 16:353–382, 1996. doi:10.1007/ BF01261321

work page 1996

[13] [13]

Gross and Jay Yellen, editors

Jonathan L. Gross and Jay Yellen, editors. Handbook of Graph Theory . Discrete Mathematics and Its Applications. CRC Press, 2003. ISBN 1- 58488-090-2; QA166.H36

work page 2003

[14] [14]

Vaibhav Karve and Anil N. Hirani. The complete set of minimal simple graphs that support unsatisﬁable 2-CNFs. Discrete Applied Mathematics ,

work page

[15] [15]

doi:10.1016/j.dam.2019.12.017

In press. doi:10.1016/j.dam.2019.12.017. 17

work page doi:10.1016/j.dam.2019.12.017 2019

[16] [16]

On subclasses of minimal unsatisﬁable formu - las

Hans Kleine B¨ uning. On subclasses of minimal unsatisﬁable formu - las. Discrete Applied Mathematics , 107(1-3):83–98, 2000. doi:10.1016/ S0166-218X(00)00245-6

work page 2000

[17] [17]

Minimal unsatisﬁability and autarkies

Hans Kleine B¨ uning and Oliver Kullmann. Minimal unsatisﬁability and autarkies. In Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisﬁability , volume 185 of Frontiers in Artiﬁcial Intelligence and Applications , chapter 11, pages 339–401. IOS Press, February 2009. doi:10.3233/978-1-58603-929-5-339

work page doi:10.3233/978-1-58603-929-5-339 2009

[18] [18]

The complexity of homomorph isms and renamings for minimal unsatisﬁable formulas

Hans Kleine B¨ uning and Daoyun Xu. The complexity of homomorph isms and renamings for minimal unsatisﬁable formulas. Annals of Mathe- matics and Artiﬁcial Intelligence , 43(1-4):113–127, 2005. doi:10.1007/ s10472-005-0422-8

work page 2005

[19] [19]

Minimal unsatisﬁability: Re- sults and open questions

Hans Kleine B¨ uning and Xishun Zhao. Minimal unsatisﬁability: Re- sults and open questions. Technical Report tr-ri-02-230, Series Com- puter Science, University of Paderborn, University of Paderborn , De- partment of Mathematics and Computer Science, 2002. http://wwwcs. uni-paderborn.de/cs/ag-klbue/de/research/MinUnsat/i ndex.html

work page 2002

[20] [20]

An application of matroid theory to the SAT prob- lem

Oliver Kullmann. An application of matroid theory to the SAT prob- lem. In Proceedings of the 15th Annual IEEE Conference on Computa- tional Complexity , pages 116–124, July 2000. See also TR00-018, Elec- tronic Colloquium on Computational Complexity (ECCC), March 2000. doi:10.1109/CCC.2000.856741

work page doi:10.1109/ccc.2000.856741 2000

[21] [21]

On Davis-Putnam reductions for min- imally unsatisﬁable clause-sets

Oliver Kullmann and Xishun Zhao. On Davis-Putnam reductions for min- imally unsatisﬁable clause-sets. Theoretical Computer Science , 492:70–87, June 2013. doi:10.1016/j.tcs.2013.04.020

work page doi:10.1016/j.tcs.2013.04.020 2013

[22] [22]

Redundancy in logic II: 2CNF and Horn propos itional formulae

Paolo Liberatore. Redundancy in logic II: 2CNF and Horn propos itional formulae. Artiﬁcial Intelligence , 172(2-3):265–299, February 2008. doi: 10.1016/j.artint.2007.06.003

work page doi:10.1016/j.artint.2007.06.003 2008

[23] [23]

Eugene M. Luks. Isomorphism of graphs of bounded valence ca n be tested in polynomial time. Journal of Computer and System Sciences , 25(1):42– 65, August 1982. doi:10.1016/0022-0000(82)90009-5

work page doi:10.1016/0022-0000(82)90009-5 1982

[24] [24]

Characterization of e ven directed graphs

Paul Seymour and Carsten Thomassen. Characterization of e ven directed graphs. Journal of Combinatorial Theory Series B , 42(1):36–45, 1987. doi: 10.1016/0095-8956(87)90061-X

work page doi:10.1016/0095-8956(87)90061-x 1987

[25] [25]

Neil J.A. Sloane. The On-Line Encyclopedia of Integer Sequence s (OEIS),

work page

[26] [26]

antipodal

Available from: http://oeis.org/. 18 A The running example The running example of the paper is based on B3, which has the following implication digraph (3 variables, thus 6 vertices, and 6 clauses, thus 2 ·6 = 12 arcs): idg(B3) = v1 →→ ↙↙ K1 v2 →→←← K2 v3 ↙↙ ←← − K3 {v1, v2}, {v1, v2}, {v2, v3}, {v2, v3}, {v1, v3}, {v1, v3} K3 v3 →→ ↗↗ − K2 v2 →→←← − K1 v...

work page

[27] [27]

U 2 n” listed below (with “U

This yields “U 2 n” listed below (with “U” for “unit”), which makes sense for n ≥ 1, and thus covers all cases with exactly two unit-clauses. To give a n overview, we list also the other three cases now (discussed below). They all generalise just the two unit-clauses. Let M := {{− 1, 2}, . . . ,{− (n − 1), n}} for n ∈ N (and with n − 1 clauses) be the inv...

work page

[28] [28]

U2 n := M ∪ {{ 1}, {− n}} for n ≥ 1

work page

[29] [29]

U1 n,i := M ∪ {{ 1}, {− n, − i}} for n ≥ 2, 1 ≤ i ≤ n − 1

work page

[30] [30]

U0 n,i := M ∪ {{ 1, i}, {− n, − i}} for n ≥ 3, 2 ≤ i ≤ n+1 2

work page

[31] [31]

For the ﬁrst case, with two units, we have shown: Lemma C.3 For F ∈ 2–MUδ=1 holds F ∼ = U2 n(F ) iﬀ F has two unit-clauses

U0 n,x,y = M ∪ {{ 1, x}, {− n, − y}} for n ≥ 4, 2 ≤ x < y ≤ n − 1, x + y ≤ n + 1. For the ﬁrst case, with two units, we have shown: Lemma C.3 For F ∈ 2–MUδ=1 holds F ∼ = U2 n(F ) iﬀ F has two unit-clauses. 23 The implication digraph of U 2 n is a cycle digraph with 2 n vertices and 2 n edges (where all vertices have degree 2). The labelled digraph, actual...

work page

[32] [32]

anti-automorphism

And from {− x, 3}, {− x, − 3}, renamed to {− x, p + 1 }, {− x, − (p + 1)}, we obtain {− x, p + 1}, . . . ,{− q, − x} for some q ≥ p + 1. Appending these chains yields with the original {− 1} a clause-set isomorphic to {− 1}, {1, 2}, . . . ,{− (n− 1), n}, {n, − i} for some 2 ≤ i < n and n ≥ 2. After ﬂipping literal 1, this is U 2 n, when adding to the last...

work page

[33] [33]

For complementary unit-clauses in F , idg(F ) is the cycle digraph of length 2, while ig( F ) is the complete graph with two vertices

work page

[34] [34]

inf” meaning “unbo unded

Equivalence-clauses {x, y}, { x, y} ∈ F yield a cycle digraph of length 2 in idg(F ), and a single edge in ig( F ). We see from the implication digraphs, that here only the ﬁrst case ha ppens, i.e., when n(F ) = 1. This is the case U 2 1, which doesn’t pose any problems. For the sequel of the proof we assume n(F ) ≥ 2, and thus no contractions happen when...

work page