Satisfiability Problem

SAT 与 UNSAT 问题

SAT

布尔可满足性问题（Boolean satisfiability problem, SAT ）询问给定 个布尔变量以及其用合取（Conjunction，）、析取（Disjunction，）和非（Not，）运算组成的布尔表达式，是否存在一种逻辑变量的赋值使得该公式为真。SAT 问题是第一个被证明是 NP 完全的问题。

为简单起见，通常要求布尔表达式以正常形式或"CNF"组合编写。CNF 格式的布尔表达式包括：

1. 由 连接的子句（clause）
2. 每个子句是由 连接的文字（literal）
3. 每个文字是一个布尔变量或布尔变量取

例如，一个由3个布尔变量以及2个子句组成的布尔表达式可以是

$(x_{1}\vee \neg x_{3}) \wedge (\neg x_{1} \vee x_{2} \vee x_{3})$

在该例中，SAT 问题需要找到 ，， 的一组赋值，如 ，， 可使得该布尔表达式为 True。

UNSAT

UNSAT 与 SAT 任务相反，需要去证明不存在一种赋值方法使布尔表达式是 True。