Solving MaxSAT and #SAT on structured CNF formulas
University of Bergen（卑尔根大学）
在本文中，我们提出了CNF公式的一个结构参数，并使用它来识别加权MaxSAT和#SAT，可以在多项式时间内解决的情况。给定一个CNF公式，我们说一个子句集是精确可满足的，如果有一些完全赋值只满足这些子句。设公式的ps值是子句的精确可满足集的个数。将分支分解的概念应用于CNF公式，并以ps值为截函数，定义了公式的ps宽度。对于一个多项式PS-宽度的分解给出的公式，我们显示动态规划算法解决加权MaxSAT和#SAT在多项式时间。结合Belmonte和Vatshelle的结果，具有结构邻域的图类和算法应用，Theor。Comput. Sci. 511：54-65（2013）'我们得到了针对某些类别的结构化CNF公式求解加权MaxSAT和#SAT的多项式时间算法。例如，我们得到了$m$子句和$n$变量的公式$F$的$O(m^2(m + n)s)$算法以及$O(m^2(m + n)s)$的大小ABMQ，如果$F$具有变量和子句的线性排序，使得对于子句$C$中出现的任何变量$x$，如果$x$出现在$C$之前，则它们之间的任何变量也出现在$C$，并且如果$C$出现在$x$之前，则$x$也出现在它们之间的任何子句中。注意，这类公式的关联图类不具有有界的宽度。
2014-02-26 cs.AI cs.CC cs.DS
A Fixed-Parameter Algorithm for Random Instances of Weighted d-CNF Satisfiability
University of British Columbia Okanagan（不列颠哥伦比亚大学奥肯那根分校）
研究了加权$d$ -CNF可满足性问题（加权$d$ -SAT）的随机情形，这是一个一般的W[1]-完全问题.该问题的随机实例由固定参数$k$和随机$d$-CNF公式$\weicnf{n}{p}{k, d}$组成，该公式如下生成：对于$d$变量的每个子集，以概率$p$，从包含至少一个否定字面值的$2^d - 1$子句中均匀随机地选择$d$变量上的子句。我们证明了加权$d$ -SAT的随机实例可以在$O(k^2n + n^{O(1)})$ -时间内以高概率求解，表明在这种实例分布下的加权$d$ -SAT的典型实例是固定参数可处理的。该结果也适用于模型$\weicnf{n}{p}{k,d}(d')$的随机实例，其中禁止包含小于$d' (1 < d' < d)$否定字面值的子句，以及在随机模型的参数$p(n)$的一定范围内的加权$d$-SAT的重整化（小型化）版本的随机实例。这一点，加上我们以前的结果的阈值行为和分辨率复杂性的$\weicnf{n}{p}{k, d}$不可满足的实例，提供了一个几乎完整的表征加权$d$ -SAT的随机实例的典型情况下的行为。
2008-06-28 cs.AI cs.CC cs.DS
Simple Reductions from Formula-SAT to Pattern Matching on Labeled Graphs and Subtree Isomorphism
CNF公式可满足性问题（CNF-SAT）在强指数时间假设（SETH）下被简化为P中的许多基本问题，以证明紧下界。最近，Abboud、Hansen、Vassilevska W.和Williams（STOC 16），以及后来的Abboud和Bringmann（ICALP 18）提出了基于一般布尔公式可满足性（Formula-SAT）的硬度的下界。从公式-SAT的约简比从CNF-SAT的通常约简有两个优点：（1）公式-SAT的困难性的说明可以说比CNF-SAT的更合理，（2）这些约简甚至对问题上界的对数改进给出了结果。在这里，我们给紧减少公式SAT的两个问题：模式匹配标记图（PMLG）和子树同构。以前从公式SAT的减少是序列比对问题，如编辑距离，LCS和弗雷歇距离，需要一些技术工作。本文使用了与以前类似的想法，但在一个明显更简单的设置，有助于说明底层技术的最显着特征。
2020-08-26 cs.CC cs.DS
Counting solutions to random CNF formulas
当随机$k$ -SAT模型的密度与$k$成指数关系时，我们给出了近似计算该模型解的个数的第一个有效算法.最好的以前的计数算法的许可版本的模型是由于蒙塔纳里和沙阿，是基于相关衰减方法，它的工作密度$(1+o_k(1))\frac{2\log k}{k}$，吉布斯的唯一性阈值的模型。相反，我们的算法利用Moitra最近的一项技术来处理随机公式。在我们的设置中的主要挑战是要考虑到高程度的变量的存在，其边缘分布是难以控制的，并导致显着的公式内的相关性。
2021-05-24 cs.DS
An Approximation Algorithm for #k-SAT
我们提出了一个简单的随机算法，近似的数量满足赋值的合取范式的布尔公式。据我们所知，这是第一个在运行时间内对任何k >= 3近似#k-SAT的算法，不仅不平凡，而且明显优于目前最快的精确算法。更确切地说，我们的算法是一个随机近似方案，其运行时间多项式依赖于误差容限，是温和的指数在输入公式的变量的数量n。例如，即使规定了次指数小的误差容限，3-CNF输入公式的解的数量也可以在时间上近似为O（1.5366^n）。对于4-CNF输入，界限增加到O（1.6155^n）。我们进一步展示了如何以可控的方式获得CNF公式的解的个数的上界和下界。放松对近似质量的要求，在k-CNF输入上，与上述界限相比，我们获得了显着减少的运行时间。
2011-07-11 cs.CC cs.DS
A Polynomial Time Bounded-error Quantum Algorithm for Boolean Satisfiability
本文的目的是回答一个长期存在的开放问题NP和BQP之间的关系。本文通过对MAX-E3-SAT问题这一基本NP难问题的BQP量子算法的提出，证明了BQP包含NP。给定一个E3-CNF布尔公式，MAX-E3-SAT问题的目标是找到最大化满足子句数量的变量分配。对于带有$m$子句的E3-CNF布尔公式，该算法在$O(m^2)$中运行，而对于带有$n$输入的E3-CNF布尔公式，在最坏情况下，该算法在$O(n^6)$中运行。该算法使用一种新的迭代部分否定和部分测量技术最大化满足条款的集合。该算法实现了任意高概率的成功$1-ε$小$ε>0$使用多项式资源。该算法除了求解MAX-E3-SAT问题外，还可以根据满足子句的最大数目来判定E3-CNF布尔公式是否可满足，这是一个NP完全问题。
2015-07-27 cs.CC cs.DS
Weighted Model Counting with Twin-Width
Bonnet等人（FOCS 2020）介绍了图不变的孪生宽度，并表明许多NP-难问题对于有界孪生宽度的图是易处理的，推广了其他宽度度量的类似结果，包括树宽和树宽。在本文中，我们研究使用孪生宽度解决命题可满足性问题（SAT）和命题模型计数。我们特别关注有界加权模型计数（BWMC），它将CNF公式$F$和有界$k$作为输入，并要求所有模型的加权和最多为$k$正文字。BWMC不仅推广SAT，而且（加权）模型计数。我们发展了CNF公式的“带符号”孪生宽度的概念，并建立了BWMC是固定参数易处理时，由认证的带符号孪生宽度$F$加上$k$参数化。我们表明，这个结果是紧的：它既不可能放弃绑定$k$，也不使用香草双宽度，而不是如果一个人希望保持固定参数的易处理性，即使是更容易的问题SAT。我们的理论结果的补充与经验评估和比较签署的双宽度上的各类CNF公式。
2022-06-03 cs.DS
FPTAS for Counting Monotone CNF
单调CNF公式是合取范式的布尔公式，其中每个变量都出现为正。我们设计了一个确定性的完全多项式时间近似方案（FPTAS），用于计算当每个变量出现在至多$5$子句中时，给定单调CNF公式的满足赋值的个数。同样，这也是一个用于计数集合覆盖的FPTAS，其中每个集合最多包含$5$元素。如果我们允许变量出现在最多个$6$子句（或包含$6$元素的集合）中，则近似它是NP困难的，因此，这给出了对单调CNF公式计数的可近似性的完整理解。这也是一个重要的一步，对所有有界度布尔#CSP问题的可逼近性的完整表征。此外，我们研究了超图匹配问题，这是自然产生的有界度布尔CSP问题的一个完整的分类，并显示了一个FPTAS计数3D匹配的超图与最大程度的$4$。我们的主要技术是相关性衰减，一个强大的工具来设计确定性的FPTAS计数问题定义的局部约束之间的一些变量。以前使用的这种设计技术分为两类：每个约束涉及最多两个变量，如一般的独立集，着色和自旋系统;或每个变量出现在最多两个约束，如一般的匹配，边覆盖和holant问题。这里研究的CNF问题具有比这些问题更复杂的结构，需要新的设计和证明技术。事实证明，我们为CNF问题开发的技术也适用于超图匹配问题。我们相信，它也可能会发现在其他CSP或更一般的计数问题的应用。
2014-04-02 cs.DS
Improving PPSZ for 3-SAT using Critical Variables
可满足CNF公式的临界变量是在所有满足赋值中具有相同值的变量。通过对CNF公式的临界变量分数进行简单的情况区分，我们将3-SAT的运行时间从Rolf [2006]的O（1.32216^n）提高到O（1.32153^n）。使用不同的方法，Iwama等人。[2010]最近实现了O（1.32113 ^n）的运行时间。我们的方法很好地结合了他们的方法，产生了目前最快的已知算法，运行时间为O（1.32065^n）。我们还将4-SAT的界从O（1.47390^n）[Iwama，Tamaki 2004]提高到O（1.46928^n），其中O（1.46981^n）可以使用[Iwama，Tamaki 2004]和[Rolf 2006]的方法获得。
2011-05-19 cs.DS
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是参数.
2012-11-30 cs.CC cs.DM cs.DS
On Problems as Hard as CNFSAT
在过去的十年中，NP难问题的精确指数时间算法领域蓬勃发展。虽然穷举搜索仍然是一些基本问题的最快算法，但对于无数问题，包括图着色，Hamilton路，支配集和3-CNF-Sat，已经发现了困难的和非平凡的指数时间算法。在某些情况下，进一步改进这些算法似乎遥不可及。CNF-Sat问题是一个典型的例子，对于这个问题，平凡穷举搜索算法在时间上运行O（2^n），其中n是输入公式中变量的数量。虽然存在CNF-Sat的非平凡算法在时间上运行o（2^n），但没有算法能够将增长率2提高到更小的常数，因此很自然地推测2是最佳增长率。Impagliazzo和Paturi [JCSS 2001]的强指数时间假设（SETH）更进一步，并断言，对于每个<1，存在一个（大）整数k，使得k-CNF-Sat不能在时间2^{n}中计算。在本文中，我们证明了，对于任何n < 1，问题击中集，集分裂，和NAE-Sat不能在时间O（2^{n}）计算，除非SETH失败。这里n是输入中元素或变量的数量。对于这些问题，我们实际上得到了某种意义上与SETH的等价。我们猜想，SETH意味着一个类似的声明集覆盖，并证明，在此假设下，最快的已知算法的Steinter树，连接顶点覆盖，集划分，和伪多项式时间算法的子集和不能显着改善。最后，我们证明了我们关于集合覆盖的硬度的假设，通过证明对于任何<1的集合覆盖数的奇偶性不能在O（2^{n}）…
2014-03-27 cs.CC cs.DM cs.DS
On the enumeration of signatures of XOR-CNF's
针对易解类CNF的最大签名高效生成这一开放问题，完整刻画了XOR-CNF的所有、最小及最大签名的生成复杂度，补充了CNF签名枚举领域的相关复杂度结论。
2025-08-04 cs.DM cs.DS math.CO
Phase transition for Local Search on planted SAT
局部搜索算法（或爬山法，或迭代改进法）是解决可满足性和最大可满足性问题的最简单的算法之一。它是许多可满足性和最大可满足性求解器的一部分，用于为更复杂的算法找到一个好的起点，并改进候选解。本文分析了随机种植3-CNF公式的局部搜索问题。我们证明了如果k<7/6使得子句与变量的比率小于kln（n）（n是CNF中变量的数量），那么局部搜索whp找不到满意的分配，如果k>7/6使得子句与变量的比率大于kln（n）$，那么局部搜索whp找到满意的分配.作为一个副产品，我们还表明，对于任何常数r有g，使本地搜索应用到一个随机的（不一定种植）3-CNF与条款变量比r产生的分配，满足至少gn条款小于最大数量的可满足的条款。
2008-11-16 cs.DS cs.LO
Further Improvements for SAT in Terms of Formula Length
在本文中，我们证明了一般的CNF可满足性问题可以在$O^*(1.0638^L)$时间内求解，其中$L$是输入CNF公式的长度（即，公式中文字的总数），改进了2009年获得的$O^*(1.0652^L)$的先前结果。我们的算法进行了分析，使用测量和征服的方法。我们的改进主要归因于以下两点：我们仔细设计了分支规则来处理度为5和度为4的变量，以避免以前的瓶颈;我们表明，一些最坏的情况不会总是发生，然后我们可以使用摊销技术，以获得进一步的改进。在我们的分析中，我们提供了一些一般的分析框架和几个下界的措施，以简化参数的减少。这些技术可以用来分析更多的基于测量和征服方法的算法。
2022-08-17 cs.DS
Almost 2-SAT is Fixed-Parameter Tractable
我们考虑以下问题。给定一个2-CNF公式，是否可以最多删除$k$子句，以使得到的2-CNF公式是可满足的？这个问题在理论计算机科学的不同研究团体中被称为“几乎2-SAT”、“除了$k$ 2-SAT之外的所有”、“2-CNF删除”、“2-SAT删除”。该问题的固定参数可处理性是参数化复杂性领域长期存在的问题。我们解决了这个问题，提出了一个算法，解决了这个问题，在$O(15^k*k*m^3)$，因此，我们表明，这个问题是固定参数听话。
2008-04-18 cs.CG cs.DS cs.LO
MAJORITY-3SAT (and Related Problems) in Polynomial Time
MIT（麻省理工学院）
多数SAT是确定合取范式（CNF）中的输入$n$变量公式是否至少具有满足赋值的$2^{n-1}$的问题。多数SAT和相关问题已经在各种对概率规划和推理的复杂性感兴趣的AI社区中得到了广泛的研究。虽然Majority-SAT被认为是PP完备的已经有40多年了，但它的一个自然变体的复杂性仍然是开放的：Majority-$k$ SAT，其中输入的CNF公式被限制为最多有$k$的子句宽度。我们证明，对于每一个$k$，多数- $k$ SAT是在P。事实上，对于任何正整数$k$和有理数$ρ\in (0,1)$与有界分母，我们给出了一个算法，可以确定是否一个给定的$k$ -CNF至少有$ρ\cdot 2^n$满足分配，在确定性线性时间（而以前最著名的算法在指数时间运行）。我们的算法有有趣的积极影响计数的复杂性和复杂性的推断，显着降低了已知的复杂性，如E-MAJ- $k$ SAT和MAJ-MAJ- $k$ SAT的相关问题。在我们的方法的核心是一个有效的方法，用于解决阈值计数问题，通过提取向日葵中发现的相应的一个$k$ -CNF集系统。我们还表明，多数- $k$ SAT的易处理性是有点脆弱。对于密切相关的GtMajority-SAT问题（我们问一个给定的公式是否有大于$2^{n-1}$满足分配），这是已知的PP-完全的，我们表明，$k$ SAT是在P的$k\le 3$，但成为NP-完全的$k\ge…
2021-11-15 cs.AI cs.CC cs.DS
SAT Backdoors: Depth Beats Size
几十年来，人们一直致力于寻找一类可满足性可以在多项式时间内判定的CNF公式。经典的结果是Horn公式（Aspvall，Plass和Tarjan，1979）和Krom（即，2CNF）公式（Dowling和Gallier，1984）。由Williams Gomes和Selman（2003）引入的后门，逐渐将这样一个易于处理的类扩展到所有与该类有界距离的公式。后门大小提供了一个公式和易处理类之间的自然但相当粗糙的距离度量。后门深度由Mählmann，Siebertz和Vigny（2021）引入，是一种更精确的距离度量，它允许并行使用不同的后门变量。有界后门大小意味着有界后门深度，但存在常数后门深度和任意大后门大小的公式。我们提出FPT近似算法计算后门深度到类霍恩和克罗姆。这导致了一个线性时间算法，用于确定这些类的有界后门深度公式的可满足性。我们基于我们的FPT近似算法上一个复杂的概念的障碍，扩展Mählmann等人。的障碍树的各种方式，包括增加分离障碍。我们通过一个新的博弈论框架，简化了后门的推理算法。最后，我们表明，有界后门深度捕获不易处理类CNF公式没有捕获任何已知的方法。
2022-02-16 cs.DS
Learning CNF formulas from uniform random solutions in the local lemma regime
School of Computing and Data Science, The University of Hong Kong（计算与数据科学学院，香港大学）；Department of Computer Science, University of California, Santa Barbara（计算机科学系，加州大学圣芭芭拉分校）；State Key Laboratory for Novel Software Technology, New Cornerstone Science Laboratory, Nanjing University（新型软件技术国家重点实验室，南京大学）
研究从均匀随机解中学习 $k$-CNF 公式的问题，通过改进 Valiant 算法显著降低了样本复杂度，并建立了精确与近似学习的信息论下界。
2025-11-04 cs.DS cs.LG stat.ML
Strong Backdoors to Bounded Treewidth SAT
Institute of Information Systems（信息系统研究所）；Vienna University of Technology（维也纳工业大学）
有多种方法可以在硬组合问题的实例中利用“隐藏结构”，以允许比一般非结构化或随机实例更快的算法。对于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）给出了任意大树宽和任意大圈割集的公式。
2012-04-27 cs.AI cs.CC cs.DM
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）。我们证明了这个问题确实…
2011-07-08 cs.DM cs.DS
Discordant Compact Logic-Arithmetic Structures in Discrete Optimization Problems
在离散优化算法效率的研究领域中，使用专用部件将某些问题多项式化约为其它问题的方法占有重要地位。本文提出了一种新的二进制序列集的紧凑表示方法，它以“紧凑三元组结构”（CTS）和“紧凑偶结构”（CCS）的形式表示，假定数据的逻辑和算术解释都是合理的。证明了在对偶解释下，任何非空的CTS表示3-CNF中的某个唯一布尔公式，表格CTS包含该公式的所有满足集，作为从相邻层中选择的三元组的连接.一般来说，任何3-CNF公式通过分解转化为不一致CTS的系统，每个CTS与由多项式算法构造的变量的单个置换相关联。因此，公式可满足性的问题归结为以下一个：确定的事实存在（或不存在）的“联合满足集”（JSS）的所有不协调结构，基于不同的排列。每个CTS到CCS的进一步变换被使用;通过对三元组级联的简单算法限制来达到保留允许集的正确性。然后，在各种结构中的“同名列的反转”的过程中，进入的目的是减少的JSS揭示的问题，在CCS系统中的零的n元组的初级检测。该公式被合成，在结构上是2-CNF的变体，与实现约束分布的多项式算法（在优化理论中众所周知）适应于通过不协调紧凑结构编码的高效求解布尔公式的计算过程相关联。
2013-09-24 cs.DS
Implicant based parallel all solution solver for Boolean satisfiability
本文发展了一种并行计算求解器，用于计算由多元布尔函数定义的布尔方程组的所有满意赋值。虽然有我们已知的CNF形式的布尔公式的可满足性的求解器，但这些主要是为了确定公式的可满足性而设计的，并且没有解决找到所有满意解的问题。而可满足性问题的并行求解器的开发仍然是计算机科学尚未完成的课题。本文提出的求解器旨在用并行算法表示布尔公式的所有解，即使没有CNF形式。将所提出的算法应用于布尔函数的代数范式（ANF）。该算法的基本思想是用布尔函数的一组完整的蕴涵式来表示满足的赋值，这些蕴涵式作为布尔公式的因子。该算法主要在公式的因子稀疏（即具有变量总数的一小部分）的情况下有效。这允许一次一个地计算单个因子的一组完整的蕴涵式，并在每一步减少公式。本文还提出了一个求ANF中函数正交蕴涵的完备集的算法。该算法的一个优点是所有的解都可以用蕴涵式来表示。最后，由于在每一步的小和分布式计算，以及在独立的线程计算，本文提出的求解器预计将是有用的开发一个良好的可扩展性的并行求解器的大规模问题的布尔可满足性在大量的处理器。
2017-02-06 cs.DS cs.LO
Backdoors to Acyclic SAT
Institute of Information Systems（信息系统研究所）；Vienna University of Technology（维也纳工业大学）
后门集（英语：Backdoor sets），是Williams等人在2003年提出的概念，是CNF公式F中的关键变量的集合，它使得求解公式变得容易;通过给后门集中的变量分配真值，公式可以简化为一个或多个多项式时间可解公式。更具体地说，F的弱后门集是变量的集合X，使得存在对X的真值赋值t，该真值赋值将F约简为属于多项式时间可判定基类C的可满足公式F[t]。强后门集是一个变量集合X，使得对于所有的赋值t到X，简化公式F[t]属于C。研究了以k为参数，在无圈关联图的CNF公式的基类上寻找最大为k的后门集的问题。我们表明，1。弱后门集的检测一般是W[2]-困难的，但对于r-CNF公式，对于任何固定的r>=3和2，固定参数是易处理的。强后门集的检测是固定参数可近似的。结果1是基类的第一个正结果，该基类不具有大小有界的障碍物的特征化。结果2是强后门集比删除后门集更强大的基类的第一个正结果。对于具有非循环关联图的CNF公式，不仅SAT，而且#SAT都可以在多项式时间内求解。因此，结果2建立了一个新的结构参数，使#SAT固定参数易于处理，并且与已知的参数（如树宽和宽度）无法比较。我们得到的算法的算法版本的Erdös-Pósa定理，Courcelle的模型检验一元二阶逻辑，以及新的组合结果如何不相交的周期可以相互作用的后门集的组合。
2012-02-21 cs.AI cs.CC cs.DS
A Randomized Algorithm for 3-SAT
在这项工作中，我们提出并分析了一个简单的随机算法，以找到一个可满足的分配的布尔公式在合取范式（CNF）在每个子句中有最多3个文字。给定n个变量的k-CNF公式phi，{0，1}^n中的alpha满足phi，如果在赋值alpha下恰好满足该子句的一个文字，则phi子句是关键的。Paturi et.等人（Chicago Journal of Theoretical计算机科学1999）提出了一种用于k-SAT的简单随机算法（PPZ），其成功概率随着关键子句的数量（相对于输入公式的固定可满足解）而增加。在这里，我们首先描述另一个简单的随机算法DEL的执行更好，如果关键条款的数量较少（相对于一个固定的可满足的解决方案的输入公式）。随后，我们结合这两个简单的算法，使得组合算法的成功概率是PPZ和DEL在每个输入实例上的成功概率的最大值。我们发现，当出现在一个或多个关键条款中的一个或多个关键条款中的每个变量的条款的平均数量在1和1.9317之间时，组合算法的性能优于PPZ算法。
2009-06-10 cs.DS math.CO
Simulating Branching Programs with Edit Distance and Friends or: A Polylog Shaved is a Lower Bound Made
最近的一项积极的工作实现了强指数时间假设（SETH）下基本问题的严格下限。Backurs和Indyk（STOC'15）的一个著名结果证明了两个长度为n的序列的编辑距离在SETH下不能在强次二次时间内计算。后续工作将结果扩展到更简单的问题，如寻找最长公共子序列（LCS）。SETH是一个非常强的假设，声称即使是线性大小的CNF公式也不能在穷举搜索上以指数加速来分析可满足性。我们认为更安全的假设，例如，这样的加速是不可能的SAT更有表现力的表示，如NC电路。直觉上，这似乎更合理：NC电路可以实现复杂的密码原语，而CNF甚至不能近似计算位的XOR。我们的主要结果是一个令人惊讶的减少从SAT分支程序的基本问题在P像编辑距离，LCS，和许多其他。真正的次二次算法，因此，这些问题的后果，我们认为是远远超过仅仅是更快的CNF SAT算法显着。例如，任意o（n）深度有界扇入电路上的SAT（因此也是NC-电路-SAT）可以在（2-eps）^n时间内求解。我们的工作的一个非常有趣的特点是，我们可以证明，即使从轻度次二次算法编辑距离或LCS的主要后果。例如，我们证明，如果我们可以从编辑距离的n^2中删除任意大的polylog因子，那么NEXP就没有非均匀的NC^1回路。更细粒度的检查表明，对于特定的常数$c \approx 10^3$，即使去除$\log^c{n}$因子，也已经意味着新的电路下限。
2015-11-18 cs.CC cs.DS
An Improved Upper Bound for SAT
我们证明了CNF可满足性问题可以用$O^*(1.2226^m)$时间求解，其中$m$是公式中子句的个数，改进了Yamamoto 15年前给出的已知上界$O^*(1.234^m)$和Hirsch 22年前给出的$O^*(1.239^m)$.通过使用摊销技术和仔细的案例分析，我们成功地避免了以前的算法中的瓶颈，并得到改进。
2020-07-08 cs.CC cs.DS
A constructive proof of the Lovasz Local Lemma
Lovasz局部引理[EL 75]是一个强大的工具，可以证明满足规定标准集合的组合对象的存在性。该技巧可直接应用于可满足性问题，得到一个k-CNF公式，其中每个子句与至多2^（k-2）个其它子句有公共变量，总是可满足的.所有迄今为止已知的证明的地方引理是非建设性的，因此不提供一个食谱，以如何一个令人满意的分配这样一个公式可以有效地found. In他的突破性论文[Bec 91]，贝克证明，如果附近的每个条款被限制为O（2^（k/48）），一个多项式时间算法的搜索问题存在。Alon简化并随机化了他的过程，并将其限制提高到O（2^（k/8））[Alo 91]。Srinivasan在[Sri 08]中提出了一个变体，其边界基本上为O（2^（k/4））。在[Mos 08]中，我们将其改进为O（2^（k/2））。本文给出了一个随机算法，该算法能为每个k-CNF公式找到一个令人满意的分配，其中每个子句的邻域最多为2^（k-5）-1个其它子句的渐近最优值，并且该算法在期望时间多项式内运行，与公式的大小无关。如果k被认为是一个常数，我们也可以给出一个确定性变量。与所有以前的方法相比，我们的分析不再调用局部引理的标准非构造性版本，因此可以被认为是它的另一种构造性证明。
2008-10-29 cs.DS
Deterministic Algorithms for the Lovasz Local Lemma
洛瓦兹局部引理（Lovasz Local Lemma，LLL）是概率论中的一个强有力的结果，它指出，如果一组坏事件的概率小于依赖于它的事件的数量，则该组坏事件中没有一个发生的概率是非零的。一个突出的应用是k-CNF公式，其中LLL意味着，如果公式中的每个子句与至多d <= 2^k/e个其他子句共享变量，则这样的公式具有令人满意的赋值。最近，Moser给出了一种有效构造满意指派的随机算法.随后，Moser和Tardos给出了一个随机算法，在一个非常一般的算法框架中构造由LLL保证的结构。我们解决了Moser和Tardos有效地去随机化这些算法留下的主要问题。具体地说，对于一个k-CNF公式，m个子句，d <= 2^{k/（1+ \eps）}/e，对于任意的\eps \in（0，1），我们给出了一个算法，找到一个满意的时间分配\tilde{O}（m^{2（1+1/ \eps）}）.这改进了Moser和Moser-Tardos的确定性算法，其运行时间为m^{Ω（k^2）}，其对于k=ω（1）是超多项式，并且改进了仅对d \leq 2^{k/16}/4起作用的其它先前算法。我们的算法在Moser和Tardos的算法框架下有效地工作于LLL的一般版本，并且也是可并行的，即，具有使用多项式多个处理器的多对数运行时间。
2019-08-05 cs.DS
Boolean Equi-propagation for Optimized SAT Encoding
Ben Gurion University of the Negev（本古里安大学）；Cadence Design Systems（楷登电子设计系统公司）；The University of Melbourne（墨尔本大学）
我们提出了一种基于传播的解决方法，布尔等传播，其中的约束建模为传播布尔文字之间的平等的信息。基于传播的求解将此信息作为部分评估的形式应用，从而得到优化的SAT编码。我们证明了各种基准测试，我们的方法在较小的CNF编码的结果，并导致加快解决时间。
2011-04-24 cs.AI cs.DS cs.LO
Constraint Satisfaction Problems Parameterized Above or Below Tight Bounds: A Survey
我们考虑约束满足问题参数化以上或以下紧的界限。一个示例是在$m/2$之上参数化的MaxSat：给定具有$m$子句的CNF公式$F$，判定是否存在至少满足$m/2+k$子句的真值赋值，其中$k$是参数。我们处理的其他问题包括MaxLin 2-AA（给定$\mathbb{F}_2$上的线性方程组，其中每个方程具有正整数权重，判定是否存在对满足总权重至少为$W/2+k$的方程的变量的赋值，其中$W$是所有方程的总权重），Max-$r$-Lin 2-AA（与MaxLin 2-AA相同，但每个方程最多具有$r$变量，其中$r$是常数）和Max-$r$-Sat-AA（给定具有$m$子句的CNF公式$F$，其中每个子句至多具有$r$文字，决定是否存在满足至少$\sum_{i=1}^m(1-2^{r_i})+k$子句的真值赋值，其中$k$是参数，$r_i$是子句$i$中的文字的数目，并且$r$是常数）。我们还考虑了Max-$r$-CSP-AA，Max-$r$-Lin 2-AA和Max-$r$-Sat-AA的自然推广，参数高于平均值的第2和第3类的序（或排列）约束满足问题以及与MaxSat有关的其他一些问题.我们讨论的结果，多项式核和参数化算法，主要是在过去几年中，以及一些开放的问题，获得的问题。
2011-08-24 cs.CC cs.DM cs.DS
A Fixed-Parameter Algorithm for #SAT with Parameter Incidence Treewidth
我们提出了一种有效的固定参数算法，用于#SAT，由关联树宽度参数化，即，二分图的树宽，其顶点是给定CNF公式的变量和子句;当且仅当变量出现在子句中时，变量和子句通过边连接。我们的算法运行时间为O（4^kklN），其中k表示关联树宽度，l表示最大子句的大小，N表示树分解的节点数。
2007-02-21 cs.CC cs.DS cs.LO
3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General
Paturi、Pudlák、Saks和Zane [1998]的PPSZ算法是唯一k-SAT的已知最快算法，其中输入公式没有一个以上的满意赋值。对于k>=5，对于一般的k-SAT也有相同的界限。我们表明，这也是k= 3，4的情况下，使用稍微修改的PPSZ算法。我们通过定义可满足的CNF公式的成本来进行分析，我们证明在每个PPSZ步骤中减少一定量。这改进了我们之前使用Moser和Scheder [2011]的最佳边界，3-SAT为O（1.308^n），4-SAT为O（1.469^n）。
2011-05-05 cs.CC cs.DS
Breaking the PPSZ Barrier for Unique 3-SAT
Paturi、Pudlák、Saks和Zane（FOCS 1998）提出的PPSZ算法是（Promise）Unique k-SAT已知的最快算法。我们给出了一个改进的算法与指数更快的界限唯一的3-SAT。对于唯一可满足的3-CNF公式，我们做以下情况区分：我们称一个子句为临界的，如果只有一个文字被唯一满足的赋值所满足。如果一个公式有许多关键子句，我们观察到PPSZ本身已经更快了。如果只有几个子句，我们使用Wahlström（ESA 2005）的算法，在这种情况下比PPSZ更快。否则，我们就得到了一个公式，其中有很少的关键条款和许多非关键条款。非关键条款至少有两个字面满意，我们将展示如何利用这一点，以提高PPSZ。
2014-02-17 cs.CC cs.DS
The Long, the Short and the Random
我们提供了坚实的证据，理论和经验，对随机稀疏$\#Ω(\log n)$ -SAT实例，它计算的精确计数满足分配在次指数时间的确定性算法的存在。该算法使用了一个很好的组合性质，每个CNF公式，它涉及到它的单调子公式的空间的不满意的分配的数量。
2020-11-08 cs.AI cs.CC cs.DM
A New Upper Bound for Max-2-Sat: A Graph-Theoretic Approach
在{ \sc MaxSat}中，我们要求一个赋值满足CNF中布尔公式的最大子句数。我们提出了一个算法，产生运行时间上界的$O^*(2^{\frac{1}{6.2158}})$为{ \sc Max-2-Sat}（每个子句包含最多2个文字），其中$K$是子句的数量。运行时间已经通过使用启发式优先级的选择上的变量，我们的分支。这些启发式优先级的实现相当简单，尽管它们对运行时间有显著的影响。该分析是使用定制的非标准措施。
2008-04-07 cs.CC cs.DM cs.DS
