浅谈 SAT 问题与 SAT-Solver
通过 Hackergame 比赛滑水知道了有 SAT-Solver 这个东西（其实是先知道了 SMT-Solver 然后再知道了 SAT-Solver），遂花了点时间去研究了一下。
这篇文章的前半部分是 SAT 相关的一些常识的回顾，后半部分开始介绍求解一般 SAT 问题的算法。
笔者计划在24春系统学习形式化方法入门内容，在那之后会进一步整理更多内容。
SAT 备件简述SAT 问题与 CNF 格式SAT 问题即可满足性问题 (Satisfiability Problem)：一般被定义为布尔可满足行问题或命题可满足性问题，即：
布尔可满足性问题 (Boolean Satisfiability Problem) ：给定布尔表达式 (由 AND, OR, NOT, 变量, 和括号构成), 是否存在对变量 TRUE 或 FALSE 的赋值, 使得整个表达式真。例如
(x + y\neg z)(x + y + z)(\neg y + \neg z)
以及：
命题可满足性问题 (Propositional satisfiability problem) :给定命题逻辑公式, 命题是否可满 ...