更新时间：2022-08-25 16:36
在计算机科学中，布尔可满足性问题（有时称为命题可满足性问题，缩写为SATISFIABILITY或SAT）是确定是否存在满足给定布尔公式的解释的问题。换句话说，它询问给定布尔公式的变量是否可以一致地用值TRUE或FALSE替换，公式计算结果为TRUE。如果是这种情况，公式称为可满足。另一方面，如果不存在这样的赋值，则对于所有可能的变量赋值，公式表示的函数为FALSE，并且公式不可满足。例如，公式“a AND NOT b”是可以满足的，因为可以找到值a = TRUE且b = FALSE，这使得（a AND NOT b）= TRUE。相反，“a AND NOT a”是不可满足的。
命题逻辑公式，也称为布尔表达式，由变量，运算符AND（连接，也用∧表示），OR（分离，∨）， NOT （否定，¬）和括号构成。如果通过为其变量分配适当的逻辑值（即TRUE，FALSE）可以使公式为TRUE，则称该公式是可满足的。给定公式，布尔可满足性问题（SAT）是检查它是否可满足。这个决策问题在计算机科学的各个领域都至关重要，包括理论计算机科学，复杂性理论，算法，密码学和人工智能。
布尔可满足性问题有几种特殊情况，其中公式需要具有特定结构。文字是一个变量，称为正文字，或变量的否定，称为负文字。子句是文字（或单个文字）的分离。如果一个子句最多包含一个正文字，则该子句称为Horn子句。如果公式是条款（或单个子句）的连接，则公式为合取范式（CNF）。例如，x1是正文字，¬x2是负文字，x1∨¬x2是子句，（x1∨¬x2）∧（¬x1∨x2∨x3）∧x1是联合范式的公式;它的第一和第三个条款是Horn条款，但它的第二个条款不是。公式是可以满足的，通过选择x1 = FALSE，x2 = FALSE和x3任意，因为（FALSE∨¬FALSE）∧（¬FALSE∨FALSE∨x3）∧FALSE求值为（FALSE∨TRUE）∧（TRUE∨FALSE ∨x3）∧FALSE，依次为TRUE∧TRUE∧FALSE（即为FALSE）。相反，CNF公式a∧¬a由一个文字的两个子句组成，是不可满足的，因为对于a = TRUE或a = FALSE，它评估为TRUE∧¬TRUE或FALSE∧¬FALSE（即，分别为FALSE）。
对于SAT问题的某些版本，定义广义联合范式公式的概念是有用的，即。作为任意多个广义子句的连接，后者对于某些布尔运算符R和（普通）文字li具有R（l1，...，ln）形式。不同的允许布尔运算符集导致不同的问题版本。例如，R（¬x，a，b）是一个广义子句，R（¬x，a，b）∧R（b，y，c）∧ R（c，d，¬z）是广义的联合正规形式。下面使用此公式，其中R是三元运算符，只有当其中一个参数为时才为TRUE。
使用布尔代数的定律，每个命题逻辑公式都可以转换为等效的连接法线形式，然而，它可以指数地更长。例如，将公式（x1∧y1）∨（x2∧y2）∨...∨（xn∧yn）转换为连接法线形式。
而前者是2个变量的n个连接的分离，后者由n个变量的2n个子句组成。
SAT是第一个已知的NP完全问题，1971年多伦多大学的Stephen Cook [2]和1973年国家科学院的Leonid Levin独立证明了这一问题。在此之前，NP完全问题的概念甚至不存在。证明显示复杂性类NP中的每个决策问题如何可以简化为CNF公式的SAT问题，有时称为CNFSAT。 Cook减少的一个有用特性是它保留了接受答案的数量。例如，确定给定图形是否具有3色是NP中的另一个问题;如果一个图表有17个有效的3色，那么Cook-Levin减少产生的SAT公式将有17个令人满意的分配。
NP完全性仅指最坏情况实例的运行时间。实际应用中出现的许多实例可以更快地解决。请参阅下面的解算SAT的算法。
如果公式仅限于析取正规形式，即它们是文字连词的脱节，那么SAT是微不足道的。当且仅当其连接中的至少一个是可满足的时，这样的公式确实是可满足的，并且当且仅当它对于某个变量x不包含x和NOT x时，连接是可满足的。这可以在线性时间内检查。此外，如果它们被限制为完全分离正常形式，其中每个变量在每个连接中恰好出现一次，则可以在恒定时间内检查它们（每个连接代表一个令人满意的分配）。但是，将一般SAT问题转换为析取范式可能需要指数时间和空间;例如，对于联合正规形式，在上述指数爆炸示例中交换“∧”和“∨”。
与任意公式的可满足性问题一样，确定公式的可满足性，其中每个条款限制为最多三个文字的连续正规形式也是NP完全的; 这个问题被称为3-SAT，3CNFSAT或3-satisfiability。为了将无限制的SAT问题减少到3-SAT，将每个子句l1∨⋯∨ln转换为n-2个子句的连接。
其中 是其他地方没有出现的新变量。虽然这两个公式在逻辑上不相同，但它们是完全可以满足的。转换所有子句得到的公式最多是其原始的3倍，即长度增长是多项式的。
3-SAT是卡普的21个NP完全问题之一，它被用作证明其他问题也是NP难的起点。这是通过从3-SAT到3-SAT的多项式时间减少来完成的。其他问题。使用此方法的问题的一个例子是clique问题：给定由c子句组成的CNF公式，相应的图由每个文字的顶点和每两个非矛盾文字之间的边组成来自不同的条款，参见图片。当且仅当公式可满足时，该图具有c-clique。
Schöning（1999）有一个简单的随机算法，该算法在时间（4/3）n中运行，其中n是3-SAT命题中的变量数，并且很有可能成功地正确决定3-SAT。
指数时间假设断言在exp（o（n））时间内没有算法可以解决3-SAT（或者实际上任何的k-SAT）（即，基本上比n中的指数更快）。
Selman，Mitchell和Levesque（1996）给出了随机生成的3-SAT公式难度的经验数据，具体取决于它们的大小参数。难度是通过DPLL算法进行的数量递归调用来衡量的。
当考虑CNF中的公式时，3个可满足性可以推广到k-可满足性（k-SAT，也就是k-CNF-SAT），每个子句包含多达k个文字。然而，因为对于任何，这个问题既不比3-SAT更容易也不比SAT更难，后两者是NP完全的，所以必须是k-SAT。
一些作者将k-SAT限制为具有k个文字的CNF公式。这也不会导致不同的复杂性类，因为每个子句l1∨⋯∨lj与j 3-可满足性问题的变体是三分之一3-SAT（也称为1-in-3-SAT和恰好1-3-SAT）。给定一个带有每个子句三个文字的连接法线形式，问题是确定是否存在对变量的真值赋值，以便每个子句只有一个TRUE文字（因此恰好是两个FALSE文字）。相反，普通的3-SAT要求每个子句至少有一个TRUE文字。正式地，三分之一的3-SAT问题作为广义联合正规形式给出，所有通用子句使用三元运算符R，如果其中一个参数是正确的则为TRUE。当三分之一的3-SAT公式的所有文字都是正数时，可满足性问题被称为三分之一正3-SAT。 三分之一的3-SAT及其正面案例在标准参考文献中列为NP完全问题“LO4”，计算机和难以理解：由Michael R. Garey和David提出的NP完全性理论指南约翰逊。作为Schaefer二分法定理的一个特例，Thomas Jerome Schaefer证明了三分之一的3-SAT是NP完全的，该定理断言任何以某种方式推广布尔可满足性的问题要么在P类中，要么是NP-完成。 Schaefer提供了一种结构，允许从3-SAT到3-SAT三分之一的简单多项式时间减少。设“（x或y或z）”是3CNF公式中的一个子句。添加六个新的布尔变量a，b，c，d，e和f，用于模拟此子句，而不是其他。那么公式R（x，a，d）∧R（y，b，d）∧R（a，b，e）∧R（c，d，f）∧R（z，c，FALSE）可满足当且仅当x，y或z中的至少一个为真时，新变量的一些设置，见图（左）。因此，任何具有m个子句和n个变量的3-SAT实例都可以被转换为具有5m子句和n + 6m变量的等于三的3-SAT实例。另一个减少只涉及四个新变量和三个子句：R（¬x，a，b）∧R（b，y，c）∧R（c，d，¬z），见图2。 自2003年以来获得显着普及的扩展是可满足模数理论（SMT），其可以通过线性约束，数组，所有不同的约束，未解释的函数，等来丰富CNF公式。这样的扩展通常保持NP完全，但是可以使用有效的求解器来处理许多这样的约束。 如果允许“for all”（∀）和“there there”（∃）量词允许绑定布尔变量，则可满足性问题变得更加困难。这种表达的一个例子是∀x∀y∃z（x∨y∨z）∧（¬x∨¬y∨¬z）;它是有效的，因为对于x和y的所有值，可以找到适当的z值，即。如果x和y都为FALSE，则z = TRUE，否则z = FALSE。 SAT本身（默认）仅使用∃量词。如果只允许∀量词，则获得所谓的重言式问题，即共同NP完全。如果允许两个量词，则该问题称为量化布尔公式问题（QBF），可以显示为PSPACE完全。人们普遍认为PSPACE完全问题比NP中的任何问题都严格，尽管尚未得到证实。使用高度并行的P系统，可以在线性时间内解决QBF-SAT问题。 普通的SAT询问是否存在至少一个使公式成立的变量赋值。各种变体处理此类任务的数量： MAJ-SAT询问所有作业的大部分是否使公式为TRUE。众所周知，PP是一种概率类。 #SAT，计算有多少变量赋值满足公式的问题，是计数问题，而不是决策问题，并且是#P-complete。 UNIQUE-SAT是确定公式是否只有一个赋值的问题。对于美国来说，它是完整的，描述了由非确定性多项式时间图灵机解决的问题的复杂性类，当只有一个非确定性接受路径时它接受并拒绝否则。 当输入限于具有至多一个令人满意的赋值的公式时，UNAMBIGUOUS-SAT是给予可满足性问题的名称。允许UNAMBIGUOUS-SAT的求解算法在具有若干令人满意的分配的公式上表现出任何行为，包括无限循环。虽然这个问题似乎更容易，但Valiant和Vazirani已经证明如果有一个实用的（即随机多项式时间）算法来解决它，那么NP中的所有问题都可以很容易地解决。 MAX-SAT是最大可满足性问题，是SAT的FNP推广。它要求最大数量的条款，任何转让都可以满足。它具有有效的近似算法，但是NP难以精确解决。更糟糕的是，它是APX完全的，意味着除非 ，否则不存在针对该问题的多项式时间近似方案（PTAS）。 其他概括包括对一阶和二阶逻辑的可满足性，约束满足问题，0-1整数规划。 SAT问题是可自我还原的，即如果SAT的实例是可解的，则正确回答的每个算法可用于找到令人满意的分配。首先，询问给定公式 的问题。如果答案是“否”，则公式不可满足。否则，询问部分实例化的公式 { }，即 ，其中第一变量 被 替换，并相应地简化。 如果答案为“是”，则 ，否则 。随后可以以相同的方式找到其他变量的值。总共需要 次算法运行，其中 是 中不同变量的数量。 这种自还原性在复杂性理论中用于几个定理：