布尔可满足性问题

在逻辑学和计算机科学中，布尔可满足性问题（有时称为命题可满足性问题，缩写为SATISFIABILITY，SAT或B-SAT）是确定是否存在一个满足给定布尔公式的解释的问题。换句话说，它问的是，一个给定的布尔公式的变量是否可以持续地被TRUE或FALSE的值取代，从而使公式的值为TRUE。如果是这样的话，这个公式就被称为可满足。另一方面，如果不存在这样的赋值，那么对于所有可能的变量赋值，该公式所表达的函数都是FALSE，该公式是不可满足的。例如，公式aANDNOTb是可满足的，因为我们可以找到a=TRUE和b=FALSE的值，这使得（aANDNOTb）=TRUE。相比之下，aANDNOTa是不可满足的。SAT是xxx个被证明是NP-complete的问题；见Cook-Levin定理。这意味着复杂度等级NP中的所有问题，包括广泛的自然决策和优化问题，最多只能像SAT一样难以解决。没有已知的算法可以有效地解决每一个SAT问题，人们普遍认为不存在这样的算法；然而这种信念还没有得到数学上的证明，解决SAT是否有多项式时间算法的问题相当于P与NP的问题，这是计算理论中一个著名的开放问题。然而，截至2007年，启发式SAT算法能够解决涉及数万个变量和由数百万个符号组成的公式的问题实例，这对于许多实际的SAT问题，如人工智能、电路设计和自动定理证明来说是足够了。

一个命题逻辑公式，也叫布尔表达式，是由变量、运算符AND（结合，也用∧表示）、OR（分离，∨）、NOT（否定，¬）和括号构成的。如果一个公式可以通过分配适当的逻辑值（即TRUE，FALSE）而变成TRUE，那么它就被认为是可满足的。布尔可满足性问题（SAT）是，给定一个公式，检查它是否可满足。这个决策问题在计算机科学的许多领域具有核心重要性，包括理论计算机科学、复杂性理论、算法学、密码学和人工智能。

一个字面是一个变量（在这种情况下，它被称为正字面）或一个变量的否定（称为负字面）。一个子句是一个字面的二连词（或一个单字面）。如果一个子句最多包含一个正字，则称为角子句。如果一个公式是子句的联结（或单个子句），则为共轭正常形式（CNF）。例如，x1是一个正字，¬x2是一个负字，x1∨¬x2是一个子句。公式(x1∨¬x2)∧(¬x1∨x2∨x3)∧¬x1是连接的正常形式；它的xxx个和第三个子句是霍恩子句，但第二个子句不是。通过任意选择x1=FALSE,x2=FALSE,和x3，这个公式是可满足的。因为(FALSE∨¬FALSE)∧(¬FALSE∨FALSE∨x3)∧¬FALSE评价为(FALSE∨TRUE)∧(TRUE∨FALSE∨x3)∧TRUE，进而评价为TRUE∧TRUE∧TRUE(即TRUE)。也就是到TRUE）。

相反，CNF公式a∧¬a，由一个字面的两个子句组成，是不可满足的，因为对于a=TRUE或a=FALSE，它分别求值为TRUE∧¬TRUE(即FALSE)或FALSE∧¬FALSE(即再次FALSE)。对于某些版本的SAT问题，定义广义共轭正常形式公式的概念是很有用的，即作为任意多的广义子句的连接，后者的形式是R(l1,...,ln)，用于一些布尔函数R和(普通)字元li。不同的允许布尔函数集会导致不同的问题版本。

2个变量的n个连接词的二择一，后者由n个变量的2n个子句组成。然而，通过使用Tseytin变换，我们可以找到一个长度与原命题逻辑公式大小成线性关系的可满足的共轭正常形式公式。