子句比变量多三个的不可满足击中子句集
Unsatisfiable hitting clause-sets with three more clauses than variables
摘要：
本文的主题是最小不可满足子句集（MU）的一致性猜想，指出对于每个固定的缺陷（子句数减去变量数），只有1000个模式，给出了一定的基本约简（广义单位子句传播）。我们把注意力集中在击中子句集（每两个子句至少有一个冲突），其中的猜想说，只有100多个同构类型。这里，已知连续性猜想对于至多亏数2成立，现在我们证明它对于亏数3成立。一个重要的工具是“（不可）约子句集”的概念：我们展示了如何减少一般问题的不可约的情况下，然后解决这种情况下（不足3）。这个概念来自数论（Korec 1984，Berger et al 1990），我们在研究中重新发现了它。
英文摘要：
The topic of this paper is the Finiteness Conjecture for minimally unsatisfiable clause-sets (MUs), stating that for each fixed deficiency (number of clauses minus number of variables) there are only finitely many patterns, given a certain basic reduction (generalising unit-clause propagation). We focus our attention on hitting clause-sets (every two clauses have at least one clash), where the conjecture says that there are only finitely many isomorphism types. The Finiteness Conjecture is here known to hold for deficiency at most 2, and we now prove it for deficiency 3. An important tool is the notion of "(ir)reducible clause-sets": we show how to reduce the general question to the irreducible case, and then solve this case (for deficiency 3). This notion comes from number theory (Korec 1984, Berger et al 1990), and we rediscovered it in our studies.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
