SAT 问题是组合优化中的一个经典问题，也是计算机科学理论与应用的一个核心问题。由于现代科技、军事以及经济管理的大量重要应用都可归结为求解NP 完全问题，而NP完全问题之间又是可以互相转化的，因此，SAT 问题的快速求解不仅具有重要的理论意义，而且在软件自动开发技术、逻辑推理机、VLSI芯片设计、优化计算以及知识库维护等诸多领域有着实际应用价值。
从算法复杂性的角度来说，SAT 问题是第一个被证明是NP完全的问题。这也就意味着，基本上任何SAT 算法都只能解决一定规模的SAT 问题，而且随着问题规模的增大，要找到有效的算法越来越难。
解决SAT 问题的最直接的方法是穷举法，也就是构造出它的真值表。由于变元的个数是有限的，而每个变元只有真和假两种取值，所以这种方法从理论上来说是可行的，但是在实际应用中显然是不合适的。例如，设有n 个变元的SAT 问题，由于布尔变量取值有0和1两种可能，所以n 个变元的取值共有2n 种可能情况。举个例子来看，设变元数为15，计算机每1ms计算一种可能（即1s计算1 000种），则要列举所有可能需要 215/1 000s（约1.0×1014 年），显然这一计算时间是无法接受的。该问题的定义如下：
定义4-3 真值指派：是一个函数t：U →{T，F}，若U 的布尔变量的个数为m，则每个真值指派为一个m 元布尔向量。
定义4-4 合取范式CNF：F=c1 ∧c2 ∧… ∧ci，其中ci 为子句，∧为合取运算符。范式F 在一真值指派t下为真，当且仅当每个子句ci 在真值指派t下为真。(www.xing528.com)
根据以上定义，则SAT 问题就是确定是否存在一真值指派t，使得布尔变量集U 上的CNF范式F 为真，若存在一真值指派t使F 为真，则称SAT 问题可满足。若F 中的每个子句的长度都为l，则称为l-SAT 问题。
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
