从CNF到DPLL算法

从三个问题出发：

  1. 什么是CNF？
  2. 如何将逻辑表达式转化为CNF？
  3. 什么是DPLL算法？

合取范式（CNF，conjunctive normal form）

CNF是指一系列逻辑表达式的合取，每一个子逻辑表达式都为下列类型之一：

转化为CNF

将普通的逻辑表达式转化为CNF需要按一下四个步骤对现有表达式进行转换：

  1. 用$ (\alpha \rightarrow \beta) \land (\beta \rightarrow \alpha) $替换$ \alpha \leftrightarrow \beta$
  2. 用$ \lnot \alpha \lor \beta$替换$ \alpha \rightarrow \beta $
  3. 替换
    1. 用$ \lnot \alpha \land \lnot \beta $替换$ \lnot (\alpha \lor \beta) $
    2. 用$ \lnot \alpha \lor \lnot \beta $替换$ \lnot (\alpha \land \beta) $
    3. 用$ \alpha$替换$ \lnot \lnot \alpha $
  4. 用$ (\alpha \lor \beta) \land (\alpha \lor \gamma) $替换$ \alpha \lor (\beta \land \gamma) $

例子

下面利用上面的步骤将一个逻辑表达式转化为CNF

$$ \begin{align*} & \qquad(p \Leftrightarrow q)\Rightarrow \lnot r\ \cr \rightarrow & \qquad ((p\Rightarrow q)\land (q\Rightarrow p)) \Rightarrow \lnot r &(1)\cr \rightarrow &\qquad \lnot ((\lnot p \lor q)\land (\lnot q\lor p))\lor \lnot r &(2)\cr \rightarrow &\qquad (\lnot(\lnot p \lor q)\lor \lnot(\lnot q\lor p))\lor \lnot r &(3.1)\cr \rightarrow &\qquad ((\lnot \lnot p\land \lnot q)\lor(\lnot \lnot q\land \lnot p)) \lor \lnot r &(3.2)\cr \rightarrow &\qquad ((p\land \lnot q)\lor(q\land \lnot p)) \lor \lnot r &(3.3)\cr \rightarrow &\qquad (p\lor q\lor \lnot r)\land(p\lor \lnot p\lor \lnot r) \land(\lnot q\lor q\lor \lnot r)\land(\lnot q\lor\lnot p\lor\lnot r) &(4) \end{align*} $$

DPLL算法

DPLL（Davis-Putnam-Logemann-Loveland）算法，是一种完备的、以回溯为基础的算法，用于解决在合取范式（CNF）中命题逻辑的布尔可满足性问题；也就是解决CNF-SAT问题。

SAT问题

布尔可满足性问题（Boolean satisfiability problem；**SAT **）属于决定性问题，也是第一个被证明属于NP完全的问题。此问题在计算机科学上许多的领域皆相当重要，包括计算机科学基础理论、算法、人工智能、硬件设计等等。

SAT问题，也叫作Boolean satisfiability problem（布尔可满足性问题），属于决定性问题。具体指给定一组布尔表达式，指定其中每个布尔变量的取值，使得布尔表达式的值为TRUE。

算法概述

SAT问题是无法再多项式时间复杂度内解决的，DPLL算法也不例外。

DPLL算法是一种搜索算法，思想与DFS十分相似，也可以说DPLL是DFS在SAT问题上的一种实现，具体实现方法就是，算法总公式中会选择一个变量，将其赋值为True,化简赋值后的表达式，如果简化的公式是可能满足的（递归），那么原公式也是可满足的；否则就将变量复制为False，重新执行一遍递归判定，若不满足，那么原公式便是不可满足的。

dpll(CS,B) { % CS==set of clauses. B=Bindings of atoms to truth values
    loop {
        if (empty(CS)) return B;
        if (emptyClause in CS) return Fail;
        if (easyCaseIn(CS,B)) [CS,B] = easyCase(CS,B);
    } % No easy cases
    CSCopy = copy(CS); BCopy=Copy(B);
    P = choose an unbound atom;
    [CSCopy, BCopy] = propagate(CSCopy, BCopy, P, True);
    answer = dpll(CSCopy,BCopy);
    if (answer != Fail) return answer;
    [CS, B] = propagate(CS, B, P, False);
    return dpll(CS,B)
}