局部引理是概率组合学和理论计算机科学的基本工具，但几乎没有任何已知的自然问题，它提供了一个渐近紧的答案。我们的论文的主题是确定这些问题中的几个，其中一对夫妇的广泛研究的极值函数相关的某些限制版本的k-SAT问题，其中的本地引理基本上是最优的答案。作为我们的主要贡献，我们构造了不可满足k-CNF公式，其中每个子句有k个不同的文字，每个变量最多出现在（2/e + o（1））*2^k/k子句中。Lopsided Local Lemma表明这是渐近最佳可能的。这个极值函数的确定是特别重要的，因为它代表了相应的k-SAT问题表现出复杂性硬度跳跃的值：从每个实例都是YES实例开始，只要允许每个变量出现在多一个子句中，它就变成了NP困难的。我们的不可满足CNF-公式的构造是基于[16]的二叉树方法，因此构造的公式属于子句比变量多一个的最小不可满足公式类MU（1）。我们的方法的主要新颖之处在于建立了一个适当的连续近似问题。这将我们引向一个微分方程，我们能够估计它的解。然后，通过离散化这个解决方案的渐近最优二叉树。构造的二叉树的重要性也通过它们在许多其他场景中的出现来强调。特别是，他们给出了渐近精确的答案，看似无关的问题，如欧洲终身制游戏介绍的杜尔[9]和搜索问题，允许有限数量的连续谎言。
英文摘要：
The Local Lemma is a fundamental tool of probabilistic combinatorics and theoretical computer science, yet there are hardly any natural problems known where it provides an asymptotically tight answer. The main theme of our paper is to identify several of these problems, among them a couple of widely studied extremal functions related to certain restricted versions of the k-SAT problem, where the Local Lemma does give essentially optimal answers.
As our main contribution, we construct unsatisfiable k-CNF formulas where every clause has k distinct literals and every variable appears in at most (2/e + o(1))*2^k/k clauses. The Lopsided Local Lemma shows that this is asymptotically best possible. The determination of this extremal function is particularly important as it represents the value where the corresponding k-SAT problem exhibits a complexity hardness jump: from having every instance being a YES-instance it becomes NP-hard just by allowing each variable to occur in one more clause.
The construction of our unsatisfiable CNF-formulas is based on the binary tree approach of [16] and thus the constructed formulas are in the class MU(1) of minimal unsatisfiable formulas having one more clauses than variables. The main novelty of our approach here comes in setting up an appropriate continuous approximation of the problem. This leads us to a differential equation, the solution of which we are able to estimate. The asymptotically optimal binary trees are then obtained through a discretization of this solution.
The importance of the binary trees constructed is also underlined by their appearance in many other scenarios. In particular, they give asymptotically precise answers for seemingly unrelated problems like the European Tenure Game introduced by Doerr [9] and a search problem allowing a limited number of consecutive lies.
