极小不可满足2-CNF的分类
Classification of minimally unsatisfiable 2-CNFs
摘要：
我们考虑极小不可满足的2-CNFs（简称2-MU）。在文献中，2-MU的特征仅限于非奇异的情况（每个变量至少出现两次正负）和带有单位子句的情况。我们提供2-MU F的完整分类。主要的工具是蕴涵有向图，我们证明了F的蕴涵有向图是一个“弱双圈”（WDC），一个小圈（可能有重叠）的大圈。结合逻辑和图论的方法，证明了WDC至多有一个斜对称，从而得到2-MU F，F'之间的同构就是它们的蕴涵有向图之间的同构.我们获得了各种应用。对于F的子句数与F的变元数之差为固定亏数k，F的自同构群为4k元二面体群的子群。对于固定的k，限制在2-MUs F上的同构问题在线性时间内是可判定的。对于固定的k，2-MU的同构类型的数量是Theta（n^（3 k-1））。斜对称WDC的平滑（线性顶点的去除）完全对应于通过1-奇异DP-约化获得的F的规范范式，这是DP-约化（或“变量消除”）的限制形式，仅约化2度的变量。这些范式的同构类型，即，斜对称WDC的同胚类型与长度为k的二元手镯（或“翻转项链”）一一对应。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
