SAT问题

1. 布尔表达式

  布尔表达式是由布尔变量和运算符（NOT , AND ,OR）所构成的表达式。

2. 布尔可满足问题

  如果对于变量的某个true,false赋值，使得一个布尔表达式的值为true，则该布尔表达式是可满足的。例如布尔公式
A = ((NOT x) AND y) OR ( x AND (NOT z))，当 x = false, y = true, z = false时，该布尔表达式值为true，则表达式A就是可满足的。可满足性问题就是判定一个给定的合取范式的布尔公式是否是可满足的。

3. SAT问题

  已知的NP-complete问题多达几百个，但作为这些问题的“祖先”，历史上第一个被证明的NP-complete问题是来自于布尔逻辑的可满足性问题（SATISFIABLITY
problem），简称为SAT。

  SAT问题是逻辑学的一个基本问题，也是当今计算机科学和人工智能研究的核心问题。工程技术、军事、工商管理、交通运输及自然科学研究中的许多重要问题，如程控电话的自动交换、大型数据库的维护、大规模集成电路的自动布线、软件自动开发、机器人动作规划等，都可转化成SAT问题。因此致力于寻找求解SAT问题的快速而有效的算法，不仅在理论研究上而且在许多应用领域都具有极其重要的意义。

  SAT的问题被证明是NP难解的问题。目前解决该问题的方法主要有完备的方法和不完备的方法两大类。完备的方法优点是保证能正确地判断SAT问题的可满足性，但其计算效率很低，平均的计算时间为多项式阶，最差的情况计算时间为指数阶，不适用于求解大规模的SAT问题。不完备的方法的优点是求解的时间比完备的方法快得多，但在很少数的情况下不能正确地判断SAT问题的可满足性。传统的方法有：枚举法、局部搜索法和贪婪算法等，但由于搜索空间大，问题一般难以求解。对于像SAT一类的NP难问题，采用一些现代启发式方法如演化算法往往较为有效。