《逻辑公式的可满足性判定——方法、工具及应用》阅读笔记

命题逻辑

命题逻辑简介

公式(formula)

命题变元是公式(称为原子公式).
如果 $φ$ 是公式,那么 $(\neg φ)$ 也是公式.
如果 $φ_{1}$ 和 $φ_{2}$ 是公式,那么 $φ_{1} * φ_{2}$ 也是公式.这里的 $*$ 表示任何一个二元连接符,常用的包括 $\lor$ , $\land$ , $\to$ , $\leftrightarrow$ .
只有上面三条规则生成的表达式是公式.

文字(literal)

原子公式或其否定为文字.原子公式本身为正文字,而原子公式的否定成为负文字.

原子公式和它的否定式互补.

子句(clause)

若干个文字的析取构成子句,长度即所含文字的个数.

只有一个文字的子句成为单子句,没有文字的子句成为空子句.

一般而言,子句的文字越多,子句越容易被满足.空子句是不可满足的.

分类

一个子句 $C$ 可以写成如下形式： $(\neg p_{1} \lor \dots \lor \neg p_{n} \lor q_{1} \lor \dots \lor q_{m}) \equiv (p_{1} \land \dots \land p_{n}) \to (q_{1} \lor \dots \lor q_{m})$ 里面的所有 $p_{i}$ 和 $q_{i}$ 都是原子公式. 蕴含符的左侧是前件(antecedent), 蕴含符的右侧是后件(consequent).

如果 $n = 0$ , 即前件为真,那么称 $C$ 为正子句;如果 $m = 0$ ,即后件为假,则称 $C$ 为负子句. 如果 $m$ 和 $n$ 都是正整数,那么称 $C$ 为混合子句.

当 $m \leq 1$ 时, 称 $C$ 为 Horn 子句, 否则成为非 Horn 子句.

合取范式(conjunctive normal form, CNF)

若干个子句的合取可称为合取范式.

合取范式 $S$ 能够被满足,当且仅当 $S$ 中的每一个子句都可以被这个赋值所满足.

可满足性问题

可满足性问题 (satisfiability problem, SAT)

一个 SAT 算法能够在有限的时间内，判定任意给定的 CNF 形式的命题逻辑公式是否可满足.

约束满足问题(constraint satisfaction problem, CSP)

给定有限个变量以及每个变量的取值范围,要求求出所有变量的值,使得一些给定的约束条件被满足. 如果每个变量的取值集合都是有限的, 这样的问题被称为有限 CSP.

显然,SAT 是 CSP 的一个特例. 同时, 有限 CSP 也可以转换为 SAT 问题, 下面介绍一个简单的方法:

假设 CSP 中的变量为 $x_{1}, x_{2}, \dots, x_{n}$ . 变量 $x_{i}$ 的取值范围是 $D_{i} = {a_{i 1}, \dots, a_{i n_{i}}}$ . 那么对于 CSP 的每个变量 $x$ 的每个可能的取值 $a$ ，引入一个布尔变元 $x : a$ . 如果这个变元为真，就代表 $x$ 的值是 $a$ .

那么对于每个变量 $x_{i}$ ，生成以下子句:

$x_{i} : a_{i 1} \lor \dots \lor x_{i} : a_{i n_{i}}$

\neg x_{i} : a_{ij} \lor \neg x_{i} : a_{ik}, (\forall j, k, 1 \leq j < k \leq n_{i})

对于每个约束条件 $C$ ，设它所含变量为 $x_{1}, \dots, x_{m}$ .生成若干个如下形式的子句, 其中每个子句对应着的是不满足约束条件 $C$ 的取值组合:

\neg x_{1} : v_{1} \lor \dots \lor \neg x_{m} : v_{m}

另外还有一种方法是把有限 CSP 的变量取值的个数用二进制展开, 例如若一个变量的取值集合的大小为 $8$ ，那么用 $3$ 个二进制位便可以进行表示. 其具体方法如下:

对于一个有着 $m$ 个取值个数的变量 $x$ , 它所需的命题变元个数为 $k = ⌈ lo g_{2} m ⌉$ . 所以我们可以用 $p_{0}, p_{1}, \dots, p_{k - 1}$ 表示 $x$ 的所有取值情况.

在一般情况下,对于命题变元 $p_{0}, p_{1}, \dots, p_{k}$ 和非负整数 $m < 2^{k}$ ,令 $L (p_{k}, \dots, p_{0}, m)$ 表示这样一个子句,它的值为假当且仅当二进制数 $(p_{k} \dots p_{0})$ 等于十进制数 $m$ . 这个子句的生成方法也很简单, 将十进制数 $m$ 展开成二进制形式,对于二进制位上的 $0$ , 用相应位的 $p$ 的正文字表示, 同理对于二进制位上的 $1$ , 用相应位的 $p$ 的负文字表示, 最后将这些文字析取起来即可.

对于每个变量 $x$ ,生成以下的子句:

L (p_{k - 1}, \dots, p_{0}, t), (\forall t, m \leq t < 2^{k})

对于每个约束条件 $C$ ,设它所含变量为 $x_{1}, \dots, x_{m}$ . 生成若干个如下形式的子句, 其中每个子句对应着的是不满足约束条件 $C$ 的取值组合:

L (p_{1, k_{1} - 1}, \dots, p_{1, 0}, v_{1}) \lor \dots \lor L (p_{m, k_{m} - 1}, \dots, p_{m, 0}, v_{m})

DPLL 算法

DPLL 算法是一种简单的基于回溯搜索法的完备算法,可以用以判定命题公式的可满足性.

在特定情况下子句集 $S$ 可以被一些策略去优化:

单子句规则 如果 $S$ 中有一个单子句 $L$ ,那么 $L$ 必须取真值,进而可以优化其他子句.
重言式规则 删去 $S$ 中的重言式. 一般可以通过检查子句中是否存在有互补的文字.
纯文字规则 如果一个文字 $L$ 的补 $\neg L$ 不在子句集 $S$ 中, $L$ 就被称作纯文字. 给纯文字赋值为真, 不会影响子句的可满足性.

此外，可以基于如下的分裂规则对 $S$ 进行分裂:

假设子句集 $S$ 可写成如下形式：

(A_{1} \lor L) \land \dots \land (A_{m} \lor L) \land (B_{1} \lor \neg L) \land \dots \land (B_{n} \lor \neg L) \land C_{1} \land \dots \land C_{ℓ} .

这里 $A_{i}, B_{j}, C_{k}$ 都是子句，且都不含 $L$ 或 $\neg L$ 。在这种情况下，我们可以生成两个比 $S$ 更简单的子句集：

S_{1} S_{2} = A_{1} \land \dots \land A_{m} \land C_{1} \land \dots \land C_{ℓ}, = B_{1} \land \dots \land B_{n} \land C_{1} \land \dots \land C_{ℓ} .

那么 $S$ 可满足，当且仅当 $S_{1}$ 可满足，或者 $S_{2}$ 可满足。

根据以上的规则, 就可以实现 DPLL 算法了.

bool DPLL(S) 
{
    while (1)
    {
        优化子句集S;
        if (无法对子句集S进行进一步优化)
        	break;
        if (S 为空) 
        	return TRUE
        if (S含有空子句)
        	return FALSE
    }
    从子句集S中选择一个文字L;
    return DP(S ∪ {L}) ∨ DP(S ∪ {¬L})
}

为了程序的效率, 一般用单子句规则优化子句集. 如果不使用任何的优化策略, DPLL 算法将会退化成朴素的枚举方法.

分支策略

在使用分裂规则时,需要选择一个文字 $L$ . 选择这个文字 $L$ 的策略就是分支策略. 简而言之有如下合适策略:

出现次数最多的变元优先
最短正子句优先
Jeroslow-Wang 对每个文字 $L$ ,定义: $J (L) = \sum_{i : L \in C_{i}} 2^{- n_{i}}$ 这里 $C_{i}$ 是第 $i$ 个子句,而 $n_{i}$ 是其长度（即该子句所含文字的个数）.在分支时，先选择 $J (L)$ 值最大的那个文字 $L$ .

Steve Paul

探索