从CNF到DPLL算法

从三个问题出发：

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

合取范式（CNF，conjunctive normal form）

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

为原子表达式（例如： $p$ ， $\lnot p$ ）
为原子表达式的逻辑或（逻辑析取）（例如： $p \lor q$ ， $p \lor \lnot q$ ）
为原子表达式（例如： $p$ ， $\lnot p$ ）
为原子表达式的逻辑或（逻辑析取）（例如： $p \lor q$ ， $p \lor \lnot q$ ）

转化为CNF

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

用 $(\alpha \rightarrow \beta) \land (\beta \rightarrow \alpha)$ 替换 $\alpha \leftrightarrow \beta\$
用 $\lnot \alpha \lor \beta\$ 替换 $\alpha \rightarrow \beta$
替换
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$
用 $(\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)
}

#从CNF到DPLL算法

#合取范式（CNF，conjunctive normal form）

#转化为CNF

#例子

#DPLL算法

#SAT问题