Unsatisfiable (k,(4*2^k/k))-CNF formulas
Heidi Gebauer
一个共轭范式的布尔公式称为（k，s）-公式，如果每个子句恰好包含k个变量，并且每个变量最多出现在s个子句中。证明了一个（k，4 *（2^k/k））-CNF公式的存在性，该公式是不可满足的.
A boolean formula in a conjuctive normal form is called a (k,s)-formula if every clause contains exactly k variables and every variable occurs in at most s clauses. We prove the existence of a (k, 4 * (2^k/k))-CNF formula which is unsatisfiable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Unsatisfiable CNF Formulas need many Conflicts
CNF公式中的一对子句构成冲突，如果有一个变量在一个子句中出现为正，在另一个子句中出现为负。没有任何冲突的CNF公式是可满足的。Lovasz局部引理暗示了一个k-CNF公式是可满足的，如果每个子句至多与2^k/e-1个子句冲突。然而，它并没有给出一个不可满足的公式在全局上有多少冲突的任何好的界限。我们证明了每个不可满足的k-CNF公式需要2.69^k个冲突，并且存在具有3.51^k个冲突的不可满足的k-CNF公式。
Unsatisfiable Linear k-CNFs Exist, for every k
我们称CNF公式为线性的，如果任何两个子句最多有一个公共变量。设线性k-SAT是判定给定的线性k-CNF公式是否可满足的问题。这里，k-CNF公式是每个子句的大小正好为k的CNF公式。已知当k >= 3时，线性k-SAT是NP-完全的当且仅当存在一个不可满足的线性k-CNF公式，并且当k >= 4时它们确实存在。我们证明了对每个k都存在不可满足的线性k-CNF公式。设f（k）是不可满足的线性k-CNF公式的最小子句数。我们证明了f（k）是Omega（k2^k）和O（4^k*k^4），即，最小尺寸不可满足线性k-CNF公式显著大于最小尺寸不可满足k-CNF公式。最后，我们证明，令人惊讶的是，线性k-CNF公式不允许一个更大的分数的条款得到满足比一般k-CNF公式。
Unsatisfiable Linear CNF Formulas Are Large and Complex
我们称CNF公式为线性的，如果任何两个子句最多有一个公共变量。我们证明了存在不超过4k^2个4^k子句的不可满足线性k-CNF公式，而任何不超过4^k/（8e^2k^2）子句的线性k-CNF公式都是可满足的.上界使用概率的方法，我们没有明确的结构来接近它，原因之一是不可满足线性公式比一般（非线性）公式表现出更复杂的结构：首先，任何不可满足线性k-CNF公式的任何树状归结反驳的大小至少为2^（2^（k/2-1））$。这意味着小的不可满足的线性k-CNF公式是Davis-Putnam型分裂算法的困难实例。其次，如果我们要求公式F有严格的归结树，即F的每个子句在归结树中只使用一次，那么我们至少需要a^a^..^ a子句，其中a约为2，该塔的高度约为k。
Small unsatisfiable $k$-CNFs with bounded literal occurrence
本文研究了有界出现次数的 $k$-CNF 子类中最小不可满足公式，结合理论论证与基于 SMS 的对称性破缺穷举搜索，确定了 3-CNF 子类的最小规模并改进了 4-CNF 的已知结果，为 MaxSAT 不可近似性提供了更强依据。
The complete set of minimal simple graphs that support unsatisfiable 2-CNFs
具有长度为2的子句（2-CNF）的合取范式的命题逻辑句子可以与多重图相关联，其中顶点对应于变量，边对应于子句。我们首先表明，每一个这样的句子，已减少，也就是说，这是不变的某些重言式的应用下，是equisatifiable的2-CNF的相关联的重图，事实上，一个单图。我们的主要结果是一个完整的表征图，可以支持不可满足的2-CNF的句子。我们证明了一个单图可以支持一个不可满足的约化2-CNF语句当且仅当它包含四个特定的小图中的任何一个作为拓扑子图。等价地，在给定的单图上支持的所有约简2-CNF语句都是可满足的当且仅当这四个图的所有子图被禁止作为原图的子图。最后，我们讨论了为什么罗伯逊-西摩图未成年人定理不适用于我们的方法。
Satisfiability Thresholds for k-CNF Formula with Bounded Variable Intersections
我们确定的阈值的变量的数量，条款的数量，条款交叉对的数量和最大条款的程度的k-CNF公式，保证满足的假设下，每两个条款共享最多$α$变量。更正式地说，我们称这些公式为$α$ -相交，并定义，例如，阈值$μ_i(k,α)$的子句交叉对$i$的数量，使得每个$α$ -相交k-CNF公式，其中最多$μ_i(k,α)$子句对共享一个变量是可满足的，并存在一个不可满足的$α$ -相交k-CNF公式与$μ_m(k,α)$这样的交叉。基于Lovasz局部引理，我们给出了这些阈值的下界，并通过构造一个不可满足的k-CNF证明了$μ_i(k,α) = \tildeΘ(2^{k(2+1/α)})$是一个几乎匹配的上界.确定了变量数量（$μ_n = \tildeΘ(2^{k/α})$）和子句数量（$μ_m = \tildeΘ(2^{k(1+\frac{1}α)})$）的类似阈值（关于该阈值的早期独立报告，请参见[Scheder 08]）。我们的上限构造给出了一个家庭的不可满足的公式，同时实现所有四个阈值。
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的二元手镯（或“翻转项链”）一一对应。
Combining the $k$-CNF and XOR Phase-Transitions
现代SAT求解器在随机$k$ -CNF公式上的运行时性能与随机$k$ -CNF公式的可满足性中经验上看到的“相变”现象密切相关。最近通用的基于散列的采样和计数方法主要依赖于SAT求解器在表示为$k$ -CNF和XOR约束的结合的公式上的运行时性能（称为$k$ -CNF-XOR公式），但是随机$k$ -CNF-XOR公式的行为在先前的工作中未被探索。本文首次研究了随机$k$ -CNF-XOR公式的可满足性。我们展示了一个令人惊讶的相变的经验证据，遵循$k$ -CNF和XOR约束之间的线性权衡。进一步证明了对于$k = 2$和（当$k$-CNF约束的数目较少时）对于$k > 2$，$k$-CNF-XOR公式存在相变.
A new upper bound for 3-SAT
我们发现，一个随机选择的3-CNF公式在n个变量与条款的变量比至少4.4898是，随着n的增长大，渐近几乎肯定不能满足。之前最好的这样的界限，由于Dubois在1999年，是4.506。自1983年以来，许多研究小组独立发现的第一个这样的界限是5.19。在此期间发表了几个在5.19和4.506之间的下降值。我们相信，我们用于证明的概率技术是独立的。
The Local Lemma is asymptotically tight for SAT
局部引理是概率组合学和理论计算机科学的基本工具，但几乎没有任何已知的自然问题，它提供了一个渐近紧的答案。我们的论文的主题是确定这些问题中的几个，其中一对夫妇的广泛研究的极值函数相关的某些限制版本的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 discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant
我们构造简单的，明确的矩阵列单位$\ell^2$规范和差异接近$1 + \sqrt{2} \approx 2.414$。这个数字给出了一个下界，最强的已知，据我们所知，常数出现在科姆洛斯猜想。给出这个界的“不可满足矩阵”是通过缩放某些不可满足布尔公式的子句变量矩阵的条目来构建的。我们表明，对于一个给定的公式，这样的缩放最大限度地提高了下界的差异可以计算与凸二阶锥程序。使用这个程序的双重证书，我们表明，我们的下界是最佳的那些使用不可满足的矩阵建立的公式承认读一次分辨率证明的不可满足性。我们还推测，这个证书的推广表明，我们的界限是最佳的所有边界使用不可满足的矩阵。
The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas
最近的基于通用散列的采样和计数方法主要依赖于SAT求解器在公式上的运行时性能，该公式表示为CNF约束和可变宽度XOR约束（称为CNF-XOR公式）的结合。在本文中，我们提出了第一次研究的运行时行为的SAT求解器配备XOR推理技术随机CNF-XOR公式。我们的经验表明，一个国家的最先进的SAT求解器的规模指数随机CNF-XOR公式在广泛的XOR条款密度，峰值周围的经验相变位置。在理论方面，我们证明了随机CNF-XOR公式的解空间在所有非零XOR子句密度下“破碎”成分离良好的组件，类似于已知许多SAT算法难以实现的随机CNF公式中的行为。
Satisfiability of Almost Disjoint CNF Formulas
我们称CNF公式为线性的，如果任何两个子句最多有一个公共变量。设m（k）是使得任何含有<= m子句的线性k-CNF公式可满足的最大整数m。我们证明了4^k/（4e^2k^3）<= m（k）<ln（2）k^44^k。更一般地，（k，d）-CSP是合取范式中的约束满足问题，其中每个变量可以取d个值中的一个，并且每个约束包含k个变量并且禁止对这些变量的d ^k个可能赋值中的恰好一个。如果没有两个不同的约束有l个或更多的共同变量，则称（k，d）-CSP l-不相交。设m_l（k，d）表示使得任意至多m个约束的l-不相交（k，d）-CSP可满足的最大整数m。我们证明了1/k（d ^k/（ed ^（l-1）k））^（1 + 1/（l-1））<= m_l（k，d）<c（k^2/lln（d）d ^k）^（1 + 1/（l-1））.对于某个常数c。这意味着对于常数l，上界和下界仅在d和k的多项式因子上不同。
Generating clause sequences of a CNF formula
给定具有子句$C_1,\ldots,C_m$和变量$V=\{x_1,\ldots,x_n\}$的CNF公式$Φ$，$Φ$的真值赋值$a:V\rightarrow\{0,1\}$导致子句序列$σ_Φ(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m$，其中$C_i(a) = 1$ if子句$C_i$在赋值$a$下求值为$1$，否则为$C_i(a) = 0$。所有可能的子句序列的集合携带关于公式的大量信息，例如SAT、MAX-SAT和MIN-SAT可以根据找到具有极值属性的子句序列来编码。我们考虑在Dagstuhl研讨会19211“数据管理中的枚举”（2019）上提出的一个问题，关于生成给定的具有有界维数的CNF的所有可能的子句序列。我们证明了问题可以在增量多项式时间内解决。我们进一步给出了这类易处理CNF公式的多项式延迟算法。我们还考虑了最大子句序列和最小子句序列的生成问题，证明了最大子句序列的生成是NP-困难的，而最小子句序列的生成具有多项式延迟。
Structure of random r-SAT below the pure literal threshold
众所周知，随机$r$ -SAT公式有一个尖锐的密度阈值可满足，而纯文字规则也有一个类似的较小阈值可满足。此外，在可满足性阈值之上，其中随机公式具有高概率（whp）不可满足性，由于大的“最小不可满足子公式”（MUF），不可满足性是whp。相比之下，我们表明，对于（罕见的）不可满足的公式低于纯文字阈值，不可满足性是由于一个独特的MUF与最小的可能的“过剩”，失败这个由于一个独特的MUF与下一个更大的过剩，等等。在同一制度下，我们给出了一个精确的渐近展开的概率，公式是不可满足的，并有效的算法满足公式或证明其不可满足性。在纯文字阈值和可满足性阈值之间发生的事情仍然是开放的。我们证明了类似的结果$k$ -核心和$k$ -着色阈值的随机图，或更一般的随机$r$ -均匀超图。
A novel weighting scheme for random $k$-SAT
考虑一个随机的$k$-CNF公式$F_{k}(n, rn)$，它具有$n$变量和$rn$子句.对于每个真值赋值$σ\in \{0, 1\}^{n}$和每个子句$c=\ell_{1}\vee\cdots\vee\ell_{k}$，令$d=d(σ, c)$为在$σ$下$c$中满足的文字出现的数量。对于固定的$β>-1$和$λ>0$，如果是$d=0$，则取$ω(σ, c)=0$;如果是$d=1$，则取$ω(σ, c)=λ(1+β)$;如果是$d>1$，则取$ω(σ, c)=λ^{d}$。应用上述加权方案，我们得到：如果$F_{k}(n, rn)$是概率趋于1的不可满足的，则$n\rightarrow\infty$，则分别对$k=3, 4, 5, 6$和$7,$有$r\geq2.83, 8.09, 18.91, 40.81, 84.87$.
On the gap between ess(f) and cnf_size(f)
给定一个布尔函数f，ess（f）表示证伪f的最大赋值集合，其中没有两个证伪f的公共蕴涵。虽然ess（f）$显然是cnf_size（f）的下界（在CNF公式中f的子句的最小数目），但Cepek等人表明它一般不是紧下界。他们给出了函数f的例子，其中ess（f）和cnf_size（f）之间有一个小的差距。我们展示了明显更大的差距。我们证明了对于任意的布尔函数，间隙可以是n中的指数，对于Horn函数，间隙可以是Theta（sqrt{n}），其中n是f的变量数。我们还引入了ess（f）的一个自然推广，我们称之为ess_k（f），它是最大的赋值集，其中没有k个赋值能证伪f的一个公共蕴涵。
Improved Bounds for Sampling Solutions of Random CNF Formulas
针对随机k-CNF公式的近似均匀解采样问题，提出近线性时间采样器，将可处理的密度界从2^{k/300}提升至2^{k/3}，首次让平均情况模型的采样可解性超越有界最大度的最坏情况模型。
Sub-exponential complexity of regular linear CNF formulas
正则线性合取范式（LCNF）公式的研究是一个有趣的问题，因为这类公式的精确可满足性（XSAT）是NP-完全的。在最近的一篇论文中，它表明，正则精确LCNF公式（XLCNF）的子类是次指数的复杂性，即XSAT可以确定在次指数的时间。在这里，我表明，这个类只是一个更大的类的LCNF公式，显示这种非常复杂的一个子集。为此，我引入LCNF公式的不相交性的性质，对于单个子句C，通过与C没有共同变量的子句的数目来测量。如果对于一个给定的LCNF公式F的所有子句具有相同的不交性d，我们称F为d-不交的，并用dLCNF表示这样的公式的类。XLCNF公式对应于特殊情况=0。本文的一个主要结果是：当d小于某个上界D时，所有d-不相交的单调l-正则LCNF公式是次指数复杂性的.这个结果可以推广到所有单调的l-正则LCNF公式F，它们具有有界平均不相交性，也具有次指数XSAT-复杂性。
The number of satisfying assignments of random regular k-SAT formulas
设$Φ$是随机$k$ -SAT公式，其中每个变量精确地出现正$d$次和负$d$次。假设$k$足够大，并且$d$略低于公式以高概率变得不可满足的临界度，我们确定满足分配的数量的对数的极限分布。
A New Bound for 3-Satisfiable MaxSat and its Algorithmic Application
设F是具有n个变量和m个子句的CNF公式. F是3-可满足的，如果对于F中的任意3个子句，存在一个满足所有子句的真值赋值。Lieberherr和Specker（1982）以及后来的Yannakakis（1994）证明了在每个3-可满足的CNF公式中，至少有2/3的子句可以被真值赋值所满足。我们改进了这一结果，证明了每个3-可满足的CNF公式F包含一个变量U的子集，使得某个真值赋值$τ$至少满足$2m/3+ m_U/3+ρn'$子句，其中m是F的子句数，m_U是F中包含来自U的变量的子句数，n'是不包含U中变量的子句中变量的总数，ρ是一个正的绝对常数. U和$τ$都可以在多项式时间内找到。我们用我们的结果表明，下面的参数化问题是固定参数的易处理的，而且，有一个线性变量数的内核。在3-S-MAXSAT-AE中，我们给出了一个3-可满足的CNF公式F，它包含m个子句，并要求我们判断是否存在至少满足2 m/3 + k个子句的赋值，其中k是参数.
On the enumeration of signatures of XOR-CNF's
针对易解类CNF的最大签名高效生成这一开放问题，完整刻画了XOR-CNF的所有、最小及最大签名的生成复杂度，补充了CNF签名枚举领域的相关复杂度结论。
The threshold for random (1,2)-QSAT
QSAT问题是SAT问题的量化版本。我们证明了随机量化扩展2-CNF公式的可满足性相转变的阈值效应的存在。我们考虑形式为$\forall X \exists Y φ(X,Y)$的布尔CNF公式，其中$X$具有$m$变量，$Y$具有$n$变量，并且$φ$中的每个子句具有来自$X$的一个文字和来自$Y$的两个文字。对于这样的公式，我们表明，阈值现象是由子句的数量和存在变量的数量$n$之间的比率控制。然后给出了相关临界比$c^{*}$的精确位置。事实上，我们证明，$c^{*}$是一个递减函数的$ α$，其中$α$是极限值的$m / \log (n)$时，$n$趋于无穷大。
Strong Backdoors to Bounded Treewidth SAT
有多种方法可以在硬组合问题的实例中利用“隐藏结构”，以允许比一般非结构化或随机实例更快的算法。对于SAT和它的计数版本#SAT，隐藏结构已经在可分解性和强后门集方面得到了利用。可分解性可以根据与给定CNF公式相关联的图的树宽来考虑，例如通过将子句和变量视为图的顶点，并使变量与其出现的所有子句相邻。另一方面，CNF公式的强后门集是一组变量，使得对该集合的每个可能的部分赋值将公式移动到固定类中，对于该固定类，（#）SAT可以在多项式时间内求解。在本文中，我们结合了上述两种方法。特别地，我们研究了在CNF公式类W_t中寻找一个小的强后门集的算法问题，其关联图的树宽至多为t。主要结果是积极的：（1）有一个时间算法，给定CNF公式F和两个常数k，t \ge 0，要么找到一个大小不超过2^k的强W_t-后门集，要么得出F没有大小不超过k的强W_t-后门集的结论。(2)有一个时间算法，给定CNF公式F，计算F的满足赋值的数目或得出sb_t（F）>k的结论，对于任何一对常数k，t \ge 0。这里，sb_t（F）表示F的最小强W_t-后门集的大小。我们的结果的意义在于，它们允许我们在算法上利用公式中的隐藏结构，这是两种方法（可分解性，后门）中的任何一种都无法访问的。在树宽1的顶部已经有一个后门大小1（即，sb_1（F）=1）给出了任意大树宽和任意大圈割集的公式。
A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and its Algorithmic Applications
如果一对单元子句的形式为$(x)$，$(\bar{x})$，则称之为冲突的。CNF公式是无单位冲突的（UCF），如果它不包含冲突的单位子句对。Lieberherr和Specker（J. ACM 28，1981）证明了对于每个具有$m$子句的UCF CNF公式，我们至少可以同时满足$\pp m$子句，其中$\pp =(\sqrt{5}-1)/2$。我们改进的Lieberherr-Specker界显示，对于每个UCF CNF公式$F$与$m$条款，我们可以找到，在多项式时间内，一个子公式$F'$与$m'$条款，使我们可以同时满足至少$\pp m+(1-\pp)m'+(2-3\pp)n"/2$条款（在$F$），其中$n"$是变量的数量在$F$中，这是不是在$F'$。我们考虑两个参数化版本的MAX-SAT，其中的参数是满足的条款以上的界限$m/2$和$m(\sqrt{5}-1)/2$的数量。前者对于一般公式是紧的，后者对于UCF公式是紧的。Mahajan和Raman（J. Algorithms 31，1999）表明，第一个参数化问题的每个实例都可以在多项式时间内转换为一个等价的问题，其中最多有$6k+3$变量和$10k$子句。我们将其改进为$4k$变量和$(2\sqrt{5}+4)k$子句。Mahajan和Raman证明了第二个参数化问题是固定参数可处理的（FPT）。我们证明了这个问题确实…
Removal of Quantifiers by Elimination of Boundary Points
我们考虑从布尔CNF公式中消除存在量词的问题。我们的方法基于以下观察。通过增加F的预解式子句消除边界点，可以消除量化CNF公式F对一组变量的依赖性。这种方法类似于[9]中描述的量词消去方法。本论文中描述的方法的差异是双重的：{ \bullet }分支仅在量化变量上执行，{ \bullet }通过调用SAT求解器来执行边界点的显式搜索。尽管我们在此之前发表了论文[9]，但从时间上讲，本报告的方法首先开发。在[10]、[11]中对该方法进行了初步介绍。由于准备专利申请，我们推迟了这种方法的出版[8]。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。