从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)
}