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

false时，该布尔表达式值为true则表达式A就是可满足的。可满足性问题就是判定一个给定的合取范式的布尔公式是否是鈳满足的

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

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

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