可满足性算法

可满足性算法（satisfiability algorithm），理学-计算机科学技术-计算机科学理论-算法-组合算法，可满足性算法是求解命题逻辑公式可满足性问题的算法。命题逻辑公式的可满足性判定问题（Propositional Satisfiability），简称SAT，是计算机科学领域的核心问题。该问题要求对一个命题逻辑公式，判定是否可以对公式中的变量赋值使得公式为真。求解SAT的算法一般接受合取范式（CNF范式）公式作为输入，即，其中每个是一个变量或者它的否，称为文字，而文字的析取构成了子句。SAT算法的目标也可以看作是判定是否存在一个赋值使得所有子句都被满足。这是一个简单的CNF公式：。SAT是第一个NP完全问题（见NP完全性），其证明者Stephen Cook因此获得了计算机领域最高奖—图灵奖。SAT算法已经被成功应用于解决许多重要问题。研究SAT问题的学者成立了一个国际SAT协会，并举办了每年一度的SAT会议，发表会议论文集。从2002年开始，SAT协会举办了国际SAT比赛，评出当前最好的SAT求解器，比赛结果在当年SAT会议上揭晓。