布尔可满足性问题查看源代码讨论查看历史
布尔可满足性问题（有时称为命题可满足性问题，缩写为SATISFIABILITY或SAT）是指在计算机科学中，是确定是否存在满足给定布尔公式的解释的问题。换句话说，它询问给定布尔公式的变量是否可以一致地用值TRUE或FALSE替换，公式计算结果为TRUE。
如果是这种情况，公式称为可满足。另一方面，如果不存在这样的赋值，则对于所有可能的变量赋值，公式表示的函数为FALSE，并且公式不可满足。例如，公式“a AND NOT b”是可以满足的，因为可以找到值a = TRUE且b = FALSE，这使得（a AND NOT b）= TRUE。相反，“a AND NOT a”是不可满足的。[1]
基本定义和术语
命题逻辑公式，也称为布尔表达式，由变量，运算符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）∧TRUE，依次为TRUE∧TRUE∧TRUE（即为TRUE）。相反，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）转换为连接法线形式。
(x1∨x2∨…∨xn) ∧
(y1∨x2∨…∨xn) ∧
(x1∨y2∨…∨xn) ∧
(y1∨y2∨…∨xn) ∧ ... ∧
(x1∨x2∨…∨yn) ∧
(y1∨x2∨…∨yn) ∧
(x1∨y2∨…∨yn) ∧
(y1∨y2∨…∨yn);
而前者是2个变量的n个连接的分离，后者由n个变量的2n个子句组成。
SAT是第一个已知的NP完全问题，1971年多伦多大学的Stephen Cook 和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问题转换为析取范式可能需要指数时间和空间;例如，对于联合正规形式，在上述指数爆炸示例中交换“∧”和“∨”。
SAT的扩展
自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整数规划。
视频
布尔可满足性问题 相关视频
参考文献
- ↑ 布尔可满足性问题（二） ，科学网 ，2009-09-12