SAT、3SAT、3-CNF-SAT问题定义

SAT (Satisfiability)问题是一类决策问题，即给定一个布尔表达式，判断是否存在一组布尔变量的赋值使得该表达式的值为真。

3SAT问题是SAT问题的一个特殊形式，即每个子句中恰好包含三个文字。例如：(x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ ¬x3) ∧ (x2 ∨ ¬x3 ∨ x4)。

3-CNF-SAT问题是3SAT问题的另一个名称，其中每个子句都是一个包含三个文字的合取范式（Conjunctive Normal Form）。例如：(x1 ∨ ¬x2 ∨ x3) ∧ (¬x1 ∨ x2 ∨ ¬x3) ∧ (x2 ∨ ¬x3 ∨ x4)。