在合取范式中很少出现的变量的界
Bounds for variables with few occurrences in conjunctive normal forms
摘要：
我们调查SAT（命题可满足性问题）和组合数学之间的连接，围绕最小程度（出现次数）的变量在各种形式的冗余的无布尔合取范式（子句集）。精益子句集没有非平凡的自给自足，也就是说，不可能满足某些子句而不触及其他子句。子句集的不足是子句数和变量数的差异。我们证明了一个精确的上界的最小可变程度的精益条款集依赖于不足。如果一个子句集不满足这个上界，那么它必须有一个非平凡的自给自足，我们表明，自给自足的减少（消除受影响的条款）可以在多项式时间内完成，而它是开放的，找到自给自足本身在多项式时间。然后我们研究了极小不可满足子句集的特殊情形的这个上界。我们表明，在这里的界可以得到改善，引入一个一般的方法来提高潜在的复发。我们考虑精确的关系，因此研究具有数论的味道。我们试图建立一个桥梁，从逻辑组合（特别是超图着色），我们彻底讨论的背景和开放的问题，并提供了许多例子和解释。
英文摘要：
We investigate connections between SAT (the propositional satisfiability problem) and combinatorics, around the minimum degree (number of occurrences) of variables in various forms of redundancy-free boolean conjunctive normal forms (clause-sets). Lean clause-sets do not have non-trivial autarkies, that is, it is not possible to satisfy some clauses and leave the other clauses untouched. The deficiency of a clause-set is the difference of the number of clauses and the number of variables. We prove a precise upper bound on the minimum variable degree of lean clause-sets in dependency on the deficiency. If a clause-set does not fulfil this upper bound, then it must have a non-trivial autarky; we show that the autarky-reduction (elimination of affected clauses) can be done in polynomial time, while it is open to find the autarky itself in polynomial time. Then we investigate this upper bound for the special case of minimally unsatisfiable clause-sets. We show that the bound can be improved here, introducing a general method to improve the underlying recurrence. We consider precise relations, and thus the investigations have a number-theoretical flavour. We try to build a bridge from logic to combinatorics (especially to hypergraph colouring), and we discuss thoroughly the background and open problems, and provide many examples and explanations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
