We call a CNF formula linear if any two clauses have at most one variable in common. We show that there exist unsatisfiable linear k-CNF formulas with at most 4k^2 4^k clauses, and on the other hand, any linear k-CNF formula with at most 4^k/(8e^2k^2) clauses is satisfiable. The upper bound uses probabilistic means, and we have no explicit construction coming even close to it. One reason for this is that unsatisfiable linear formulas exhibit a more complex structure than general (non-linear) formulas: First, any treelike resolution refutation of any unsatisfiable linear k-CNF formula has size at least 2^(2^(k/2-1))$. This implies that small unsatisfiable linear k-CNF formulas are hard instances for Davis-Putnam style splitting algorithms. Second, if we require that the formula F have a strict resolution tree, i.e. every clause of F is used only once in the resolution tree, then we need at least a^a^...^a clauses, where a is approximately 2 and the height of this tower is roughly k.
局部引理是概率组合学和理论计算机科学的基本工具，但几乎没有任何已知的自然问题，它提供了一个渐近紧的答案。我们的论文的主题是确定这些问题中的几个，其中一对夫妇的广泛研究的极值函数相关的某些限制版本的k-SAT问题，其中的本地引理基本上是最优的答案。作为我们的主要贡献，我们构造了不可满足k-CNF公式，其中每个子句有k个不同的文字，每个变量最多出现在（2/e + o（1））*2^k/k子句中。Lopsided Local Lemma表明这是渐近最佳可能的。这个极值函数的确定是特别重要的，因为它代表了相应的k-SAT问题表现出复杂性硬度跳跃的值：从每个实例都是YES实例开始，只要允许每个变量出现在多一个子句中，它就变成了NP困难的。我们的不可满足CNF-公式的构造是基于[16]的二叉树方法，因此构造的公式属于子句比变量多一个的最小不可满足公式类MU（1）。我们的方法的主要新颖之处在于建立了一个适当的连续近似问题。这将我们引向一个微分方程，我们能够估计它的解。然后，通过离散化这个解决方案的渐近最优二叉树。构造的二叉树的重要性也通过它们在许多其他场景中的出现来强调。特别是，他们给出了渐近精确的答案，看似无关的问题，如欧洲终身制游戏介绍的杜尔[9]和搜索问题，允许有限数量的连续谎言。
QSAT问题是SAT问题的量化版本。我们证明了随机量化扩展2-CNF公式的可满足性相转变的阈值效应的存在。我们考虑形式为$\forall X \exists Y φ(X,Y)$的布尔CNF公式，其中$X$具有$m$变量，$Y$具有$n$变量，并且$φ$中的每个子句具有来自$X$的一个文字和来自$Y$的两个文字。对于这样的公式，我们表明，阈值现象是由子句的数量和存在变量的数量$n$之间的比率控制。然后给出了相关临界比$c^{*}$的精确位置。事实上，我们证明，$c^{*}$是一个递减函数的$ α$，其中$α$是极限值的$m / \log (n)$时，$n$趋于无穷大。
