从三个问题出发:

  1. 什么是CNF?
  2. 如何将逻辑表达式转化为CNF?
  3. 什么是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需要按一下四个步骤对现有表达式进行转换:

  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\)替换\(\lor \lor \alpha\)
  4. 用\((\alpha \lor \beta) \land (\alpha \lor \gamma)\)替换\(\alpha \lor (\beta \land \gamma)\)

例子

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

$$$latex
\begin{align} & \qquad(p \Leftrightarrow q)\Rightarrow \lnot r\ \rightarrow &\qquad ((p\Rightarrow q)\land (q\Rightarrow p)) \Rightarrow \lnot r &(1)\ \rightarrow &\qquad \lnot ((\lnot p \lor q)\land (\lnot q\lor p))\lor \lnot r &(2)\ \rightarrow &\qquad (\lnot(\lnot p \lor q)\lor \lnot(\lnot q\lor p))\lor \lnot r &(3.2)\ \rightarrow &\qquad ((\lnot \lnot p\land \lnot q)\lor(\lnot \lnot q\land \lnot p)) \lor \lnot r &(3.1)\ \rightarrow &\qquad ((p\land \lnot q)\lor(q\land \lnot p)) \lor \lnot r &(3.3)\ \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 problemSAT )属于决定性问题,也是第一个被证明属于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)
}
最后修改日期: 2022-03-20