SAT 求解器可以求解一个布尔公式是否存在成真赋值
CDCL (Conflict-Driven Clause Learning) 是一种 SAT 求解算法
求解
用基于 CDCL 实现的 SAT 求解器求解布尔公式：
\phi = (x_1 \lor \lnot x_2) \land (\lnot x_1 \lor x_3) \land (\lnot x_3 \lor \lnot x_2) \land (\lnot x_1 \lor \lnot x_2)
决策
CDCL 选择一个未被赋值的变量做出假设，假设选择 x_1 = \text{True}
传播
传播当前的赋值，看能否决定其他变量的值：
考察第一个子句 x_1 \lor \lnot x_2，已经为真
考察第二个子句 \lnot x_1 \lor x_3，若要使其为真，只能是 x_3 = \text{True}
更新赋值：\{ \ x_1 = \text{True}, \ x_3 = \text{True}\ \}
考察第三个子句 \lnot x_3 \lor \lnot x_2，若要使其为真，只能是 x_2 = \text{False}
更新赋值：\{ \ x_1 = \text{True}, \ x_2 = \text{False}, \ x_3 = \text{True}\ \}
冲突检测
边传播边考察当前赋值导致冲突
当前已考察过前三个子句，都没发现冲突，考察最后的第四个子句：\lnot x_1 \lor \lnot x_2，值为真，也没有产生冲突
解决冲突
如果发现冲突，识别导致冲突的变量组合，然后生成一个新的“冲突子句”并将其加入公式中，以避免以后再遇到相同的冲突
例如，如果 \{ \ x_1 = \text{True}, \ x_3 = \text{True}\ \} 这一组合导致冲突，则生成一个新子句 \lnot x_1 \lor x_3，并回溯到一个安全状态重新决策
（决策变量是根据其优先级选择的。每当发生冲突时，子句中每个变量的优先级都会提高。为此，最近参与冲突的变量更有可能被选为决策变量）
终止
如果没有冲突且所有子句都被满足，则算法终止，并找到所求公式的一组成真赋值
如果冲突无法解决，则说明该公式不存在成真赋值
上述公式的一组成真赋值为：\{ \ x_1 = \text{True}, \ x_2 = \text{False}, \ x_3 = \text{True} \ \}
写成布尔公式的形式是：x_1 \land \lnot x_2 \land x_3