SAT Solver

Algorithm 1 (Brute force SAT solver). Given a partial truth assignment $\mathcal{J}$, determine whether we can expand it into a total one which satisfies $\phi$.
$BF(\mathcal{J})$:

• if $\mathcal{J}$ is a total assignment and $\llbracket\phi\rrbracket_{\mathcal{J}} = \mathbf{T}$, return SAT
• if $\mathcal{J}$ is a total assignment and $\llbracket\phi\rrbracket_{\mathcal{J}} = \mathbf{F}$, return UNSAT
• if $\mathcal{J}$ is not a total assignment
  • pick a propositional variable $p$ which is not assigned a value by $\mathcal{J}$
  • execute $BF(\mathcal{J} \cup [p \mapsto \mathbf{T}])$ and $BF(\mathcal{J} \cup [p \mapsto \mathbf{F}])$
  • return SAT if one of the above answers SAT, return UNSAT otherwise

Optimization: A conflict may be detected on a partial assignment!
这种方法就相当于用递归的方式遍历所有可能的 $\mathcal{J}$。

Example:

$$(p_{1} \lor \neg p_{4}) \land (\neg p_{2} \lor p_{3}) \land (p_{2} \lor p_{4}) \land (\neg p_{2} \lor \neg p_{3} \lor p_{4}) \land (\neg p_{1} \lor \neg p_{4})$$

$$\mathcal{J} = [p_{1} \mapsto \mathbf{T}, p_{4} \mapsto \mathbf{T}]$$

Algorithm 2. $BF^{+}(\mathcal{J})$:

• if $\mathcal{J}$ causes a conflict on $\phi$, return UNSAT
• otherwise, if $\mathcal{J}$ is a total assignment, return SAT
• otherwise,
  • pick a propositional variable $p$ which is not assigned a value by $\mathcal{J}$
  • execute $BF^{+}(\mathcal{J} \cup [p \mapsto \mathbf{T}])$ and $BF^{+}(\mathcal{J} \cup [p \mapsto \mathbf{F}])$
  • return SAT if one of the above answers SAT, return UNSAT otherwise

和上一种方法相比，这种方法能够在 partial truth assignment $\mathcal{J}$ UNSAT 的时候退出，减少了枚举数量。

Unit Propagation (赋值推导): In one clause, if all literals except one are false, the last one must be true.
Example:

$$\begin{aligned} & (p_{1} \vee \neg p_{4}) \wedge \boldsymbol{(\neg p_{2} \vee p_{3})} \wedge (p_{2} \vee p_{4}) \wedge (\neg p_{2} \vee \neg p_{3} \vee p_{4}) \wedge (\neg p_{1} \vee \neg p_{4}) \quad \mathcal{J} = [p_{2} \mapsto \mathbf{T}] \\ \Rightarrow & \quad \mathcal{J}(p_{3}) \text{ should be } \mathbf{T} \\ \Rightarrow & \quad (p_{1} \vee \neg p_{4}) \wedge (\neg p_{2} \vee p_{3}) \wedge (p_{2} \vee p_{4}) \wedge \boldsymbol{(\neg p_{2} \vee \neg p_{3} \vee p_{4})} \wedge (\neg p_{1} \vee \neg p_{4}) \quad \mathcal{J} = [p_{2} \mapsto \mathbf{T}, p_{3} \mapsto \mathbf{T}] \\ \Rightarrow & \quad \mathcal{J}(p_{4}) \text{ should be } \mathbf{T} \end{aligned}$$

Algorithm 3 (DPLL($\mathcal{J}$)).

• let $\mathcal{J}'$ be UnitPro($\mathcal{J}$)
• if $\mathcal{J}'$ causes a conflict on $\phi$, return UNSAT
• otherwise, if $\mathcal{J}'$ is a total assignment, return SAT
• otherwise,
  • pick a propositional variable $p$ which is not assigned a value by $\mathcal{J}'$
  • execute DPLL($\mathcal{J}' \cup [p \mapsto \mathbf{T}]$) and DPLL($\mathcal{J}' \cup [p \mapsto \mathbf{F}]$)
  • return SAT if one of the above answers SAT, return UNSAT otherwise

利用了赋值推导的算法，进一步减少了需要枚举的情况。

Algorithm 4 (CDCL, Conflict Driven Clause Learning).
矛盾驱动的子句学习方法。

• let $\mathcal{J}$ be the empty assignment at the beginning
• set $\mathcal{J}$ to UnitPro($\mathcal{J}$)
• if $\mathcal{J}$ causes a conflict on $\phi$
  • let $D$ be the result of ConflictClauseGen()
  • if $D$ is an empty clause, return UNSAT
  • add $D$ to the CNF
  • remove assignments after the second last “Pick” in $D$ from $\mathcal{J}$
  • go back to step 2 (the unit propagation step)
• otherwise, if $\mathcal{J}$ is a total assignment, return SAT
• otherwise,
  • pick a propositional variable $p$ which is not assigned a value by $\mathcal{J}$
  • pick a truth value $t \in \{\mathbf{T}, \mathbf{F}\}$
  • set $\mathcal{J}$ to ($\mathcal{J} \cup [p \mapsto t]$)
  • go back to step 2 (the unit propagation step)

这种方法会不断增加子句的数量。例如：

$$\begin{aligned} &p_{1}\vee p_{5}\\&\neg p_{1}\vee p_{7}\\&p_{2}\vee p_{4}\vee\neg p_{9}\\&\neg p_{2}\vee p_{9}\vee\neg p_{10}\\&\neg p_{3}\vee\neg p_{8}\\&p_{4}\vee\neg p_{5}\vee\neg p_{7}\\&\neg p_{6}\vee p_{9}\\&p_{6}\vee p_{10}\\&\neg p_{7}\vee p_{8}\vee\neg p_{9}\vee p_{10}\\&\neg p_{9}\vee\neg p_{10} \end{aligned}$$

可以发现 $\mathcal{J}(p_1)$ 决定 $\mathcal{J}(p_7)$；$\mathcal{J}(p_3)$ 决定 $\mathcal{J}(p_8)$；$\mathcal{J}(p_6)$ 决定 $\mathcal{J}(p_9)$ 决定 $\mathcal{J}(p_{10})$。当 $\mathcal{J}(p_1)=\mathcal{J}(p_3)=\mathcal{J}(p_6) = T$，会导致 $\llbracket \lnot p_7 \lor p_8 \lor \lnot p_9 \lor p_{10} \rrbracket_{\mathcal{J}} = F$，矛盾。因此引入了子句 $\lnot p_1 \lor \lnot p_3 \lor \lnot p_6$。