计算机科学可满足性问题本页总览可满足性问题定义一个布尔公式是用布尔变量和操作构建的表达式，它的满足性问题是确定一个表达式是否存在一个给变量的赋值以使该表达式为 1。 SAT={⟨ϕ⟩∣ϕ is a satisfiable Boolean formula }S A T=\{\langle\phi\rangle \mid \phi \text { is a satisfiable Boolean formula }\}SAT={⟨ϕ⟩∣ϕ is a satisfiable Boolean formula } 特别地，3-SAT 也是 NP 完全的。 计数形式 #SAT={⟨ϕ,k⟩∣ϕ is a cnf-formula with exactly k satisfying assignments }\# S A T=\{\langle\phi, k\rangle \mid \phi \text { is a cnf-formula with exactly } k \text{ satisfying assignments }\}#SAT={⟨ϕ,k⟩∣ϕ is a cnf-formula with exactly k satisfying assignments }