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公式中的行为。
2017-10-17 cs.CC cs.DM
The Relative Exponential Time Complexity of Approximate Counting Satisfying Assignments
研究了满足CNF赋值的近似计数的指数时间复杂度。我们把问题归结为CNF的可满足性问题。我们的减少保留了输入公式的变量数量，因此也保留了近似计数的指数复杂性。我们的算法也类似于一个算法，该算法在实践中工作得特别好，但没有近似保证是已知的。为了分析我们的还原，我们提供了一个新的不等式类似的Bonami-Beckner超压缩不等式。
2012-08-13 cs.CC
Understanding model counting for $β$-acyclic CNF-formulas
ENS Cachan（卡尚高等师范学校）；Inria（法国国家信息与自动化研究所）；Université Paris Diderot（巴黎狄德罗大学）；Ecole Polytechnique（巴黎综合理工学院）
我们扩展了知识，所谓的结构限制的$\mathrm{\#SAT}$给出了一个多项式时间算法的$β$ -无循环$\mathrm{\#SAT}$。与以前的算法在该地区，我们的算法不进行动态规划，但沿消除顺序，解决了加权版本的约束满足。此外，我们给出的证据表明，这种偏离更标准的算法是不是一个巧合，但有可能没有动态规划算法的通常风格的$β$ -非循环$\mathrm{\#SAT}$。
2014-05-23 cs.AI cs.CC
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
Knowledge Compilation, Width and Quantification
在量化布尔公式（QBF）的背景下，我们推广了关于SAT和#SAT在有界树宽CNF-公式上的易处理性的许多结果。为此，我们从研究OBDD的宽度概念开始，并观察到OBDD中存在或普遍投影一个变量块时大小的爆炸只影响其宽度。然后，我们将宽度的概念推广到结构化（确定性）DNNF的更一般的表示，并给出了一个类似的算法来存在或普遍投影一个变量块。使用一个众所周知的算法转换有界树宽CNF公式到确定性DNNF，我们能够将这种连接推广到量化CNF，这给了我们一个副产品，人们可以在FPT时间内计算有界树宽和有界量词交替量化CNF的模型数量。我们也给出了一个广泛的研究有界宽度d-DNNF，并证明了我们的几个结果的最优性。
2018-07-11 cs.CC
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
Compression with wildcards: All models of a Boolean 2-CNF
提出 A-I-I 算法，以使用无关符号的压缩格式枚举偏序集的图独立序理想，可并行化并适应多项式总时间算法枚举布尔 2-CNF 模型集，在多项实例中优于 Mathematica 内置命令。
2025-04-06 cs.CC
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
Projective cofactor decompositions of Boolean functions and the satisfiability problem
给出了一个CNF公式$F$，给出了一个判定$F$的可满足性（SAT）和计算所有赋值解的新算法.该算法基于文献中已知的\emph{cofactors}的概念。本文是作者以前的工作布尔可满足性\cite{sul1, sul2,sude}的一个后果，但该算法基本上是独立的正交扩展概念，以前的论文是基于。该算法通过将搜索空间投影到满足公式中CNF的集合上，递归地选择一个具体的余因子。该辅因子称为\emph{projective cofactor}。这样的计算的优点是，它递归地分解成独立的子问题在每一个选择的投影余因子的可满足性问题。这导致了一个并行算法，以确定可满足性和计算所有解决方案的可满足公式。
2017-05-08 cs.CC
XSAT of Linear CNF Formulas
解决了与正则性和均匀性有关的线性CNF公式的计算复杂性的未决问题。特别地，证明了任意l-正则单调CNF公式是XSAT-不可满足的，如果它的子句数m不是l的倍数.对于精确的线性公式，人们惊奇地发现l-正则性蕴含k-一致性，其中m = 1 + k（l-1）），并且允许的k-值服从k（k-1）= 0（mod l）。然后可以确定这类单调精确线性和l-正则CNF公式关于XSAT的计算复杂性：如果m不是l的倍数，则XSAT-可满足性是平凡的，或者可以在次指数时间内确定，即O（exp（n^^1/2））.次指数的时间行为的更广泛的一类定期和一致的线性CNF公式可以显示某些子类。
2018-01-18 cs.CC math.LO
Small unsatisfiable $k$-CNFs with bounded literal occurrence
本文研究了有界出现次数的 $k$-CNF 子类中最小不可满足公式，结合理论论证与基于 SMS 的对称性破缺穷举搜索，确定了 3-CNF 子类的最小规模并改进了 4-CNF 的已知结果，为 MaxSAT 不可近似性提供了更强依据。
2024-07-19 cs.CC cs.DM cs.LO
On the Satisfaction Probabilities of $k$-CNF Formulas
本文针对 $k$CNF 公式满足概率问题 $k$SAT-Pr$_{>p}$ 给出完整三分法刻画，证明其属于 AC$^0$、NL-完全或 NP-完全，并基于最大满足概率公式的存在性建立核化、后门集和局部性等关键性质。
2024-08-09 cs.CC cs.LO
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
Polynomial Time Algorithm for Boolean Satisfiability Problem
本文证明集合特殊覆盖相关算法过程具有多项式时间复杂度，并提出一个判定 CNF 布尔函数可满足性的多项式时间算法，其复杂度以输入长度立方为上界，且在 Python 实现中通过了数万变量和从句规模的测试。
2023-10-28 cs.CC
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
Trading inference effort versus size in CNF Knowledge Compilation
知识编译（KC）研究布尔函数f到某种形式F的编译，它允许在多项式时间内回答某种类型的所有查询。由于它与SAT求解的相关性，我们集中在查询类型"子句蕴涵"（CE）上，即，子句C是否从f得出，我们考虑CNF的子类，即，具有特殊性质的子句集F。在此报告中，我们不允许辅助变量（Outlook除外），因此F需要等效于f。我们考虑层次UC_k <= WC_k，这是作者在2012年引入的。每个级别都允许CE查询。前两个级别是KC的知名课程。即UC_0 = WC_0与KC中研究的PI相同，即f由所有素蕴涵的集合表示，而UC_1 = WC_1与del Val（1994）引入的单位反驳完备子句集类UC相同。我们发现，对于每一个k有（序列）布尔函数的polysize表示在UC_{k+1}，但与WC_k表示的指数下界。这种分离以前只知道k = 0。我们还考虑了传播完备子句集类PC <UC。我们发现，有（序列）布尔函数的polysize表示在UC，而有一个指数下界表示在PC。这些分离是迈向确定层次结构PC_k <UC_k <= WC_k的表示能力的一般猜想的步骤。这个猜想的强形式也允许辅助变量，正如在展望中深入讨论的那样。
2013-11-08 cs.CC
Hardness Amplification in Proof Complexity
我们提出了一个通用的方法转换任何家庭的不可满足的CNF公式，这是很难的最简单的证明系统，树分辨率，到公式，需要大的排名在任何证明系统，操作多项式或多项式阈值函数的次数最多为k（被称为Th（k）证明）。这些系统包括Lovasz-Schrijver和Cutting Planes证明系统以及它们的高度类似物。这些是基于分析两个新的证明系统，表示为T^cc（k）和R^cc（k）。T^cc（k）的证明线是任意的布尔函数，其中的每一个都可以通过有效的k方随机通信协议来评估。它们包括Th{k-1}证明作为特殊情况。R^cc（k）证明是更强的，并且只要求每个推理可以通过有效的k方随机通信协议进行局部检查。（1）当k为O（loglogn）时，对任何要求分辨秩r的不可满足CNF公式F，在所有R^cc（k）系统中存在一个要求反驳秩r^Omega（1/k）log^O（1）n的CNF公式G=Lift_k（F）. (2)当k为O（loglogn）时，T^cc（k）和R^cc（k）系统关于k存在严格的层次，因为存在需要大秩R^cc（k）反驳但具有log^O（1）n秩Th（k）反驳的不可满足CNF公式. (3)当k为O（loglogn）时，大类提升CNF公式的树型T^cc（k）反驳的大小有2^（n^Omega（1/k））个下界. (4)基于低秩分辨率的相关间隙，为低秩R^cc（2）推断（以及因此切割平面和Th（1…
2009-12-03 cs.CC
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
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 Critique of Du's "A Polynomial-Time Algorithm for 3-SAT
本文批评Du提出的3-SAT多项式时间算法，指出其算法存在缺陷，会错误判定无限族可满足3-CNF公式为不可满足，因而未能证明P=NP。
2024-04-05 cs.CC
Algorithm that Solves 3-SAT in Polynomial Time
复杂性类P是否等于复杂性类NP的问题在过去的40年里一直是一个看似棘手的问题。很明显，如果存在一种算法，可以在多项式时间内解决NP类问题，那么P将等于NP。然而，还没有人能够创建该算法或成功证明这样的算法不存在。本文提出的算法解决了3-可满足性或3-CNF-SAT问题，该问题已被证明是NP-完全的。
2015-06-02 cs.CC
Exponential Time Complexity of the Permanent and the Tutte Polynomial
我们证明了充分研究的#P-hard问题的条件下界：（a）具有n个变量的2-CNF公式的满足赋值的数量不能在时间exp（o（n））中计数，并且对于计算n-顶点图中所有独立集的数量也是如此。(b)元素为0和1的n × n矩阵的积式不能在时间exp（o（n））中计算。(c)一个n-顶点多重图的Tutte多项式在多重图的情况下在大多数赋值点（x，y）处不能在时间exp（o（n））中计算，在简单图的情况下不能在时间exp（o（n/polylog n））中计算.我们的下界是相对于指数时间假设（ETH）的（变体），它说n-变量3-CNF公式的可满足性不能在时间exp（o（n））中确定。我们通过引入它的计数版本#ETH来放松这个假设，即满意的分配不能在时间exp（o（n））中计数。为了使用#ETH作为我们的下界，我们将d-CNF公式的稀疏化引理转移到计数设置中。
2012-06-08 cs.CC cs.DS math.CO
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
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-复杂性。
2018-12-21 cs.CC cs.DM math.LO
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
Solving MaxSAT by Successive Calls to a SAT Solver
Cairo University（开罗大学）
最大可满足性（MaxSAT）问题是在合取范式（CNF）中找到使给定布尔公式的满足子句的数目最大化的真值分配的问题。近年来，MaxSAT的许多精确求解器已经开发出来，其中许多都在著名的SAT会议上发表。MaxSAT的算法一般分为两类：（1）分支定界算法和（2）连续调用SAT求解器的算法（基于SAT的），在实际问题中，基于SAT的算法被证明是更有效的。本文提供了一个实验研究，以比较最近的SAT为基础的分支定界算法的MaxSAT评估基准的性能。
2016-03-11 cs.AI cs.CC cs.LO
