SAT问题，即可满足性问题（Boolean Satisfiability Problem），是理论计算机科学中的一个重要问题。它涉及判断一个由布尔变量组成的命题公式是否可满足，即是否存在一种赋值方式，使得所有子句中的布尔表达式都为真。

基本概念

布尔变量：只有两个值，0和1。

命题公式：由布尔变量和逻辑运算符（AND、OR、NOT）组成的公式。

CNF公式：谓词逻辑中的一种公式形式，每个子句都是合取（AND）形式，整个公式是析取（OR）形式。

问题形式

k-SAT：其中k是子句中变量的最大数量。当k>2时，问题被认为是NP完全的。

2-SAT：是k-SAT的一个特例，其中每个子句最多包含两个变量，并且这些变量不能同时取真。

重要性

理论意义：SAT问题是第一个被证明为NP完全的问题，对NP完全问题的理论研究具有重要意义。

实际应用：SAT问题在约束满足问题（Constraint Satisfaction Problem, CSP）中非常普遍，并在实际生产中有广泛应用。

解决方法

完备性算法：如回溯法，可以保证找到解（如果存在），但计算效率低，不适合大规模问题。

非完备性算法：如爬山法、模拟退火、遗传算法等，可以在合理时间内找到近似解或良好解。

转化问题模型

将所有变量的赋值方案记为a={a1,a2,…,an}，原问题转化为判断某个函数（如最小值）是否能达到0。