常文静，徐 扬，吴贯锋

CHANG Wenjing1，3,XU Yang2，3,WU Guanfeng1，3

1.西南交通大学 信息科学与技术学院，成都 610036

2.西南交通大学 数学学院，成都 610036

3.系统可信性自动验证国家地方联合工程实验室，成都 610036

1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610036,China

2.School of Mathematics,Southwest Jiaotong University,Chengdu 610036,China

3.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610036,China

1 引言

布尔可满足问题（Boolean Satisfiability Problem，SAT问题）是首个被证明是NP完全的问题[1]，具有十分重要的理论意义。布尔变量x可以被赋值为true（1）或false（0），由一个或多个变量的析取组成一个子句，若子句中至少存在一个变量赋值为1，则该子句是可满足的。由一个或多个子句的合取构成合取范式（Conjunction Normal Form，CNF），SAT问题一般可转化成CNF表示。判定SAT问题的满足性是指若存在一组变量赋值{x1,x2,…,xN}（N为子句集F中的变量个数），使得子句集F中所有的子句都是可满足的，则子句集F是可满足的，或者给出证明，对于变量的任何赋值，子句集F都是不可满足的。近年来，SAT问题的判定技术也应用在实际领域中，如人工智能规划（AI Planning）、定理证明、软件及硬件验证、集成电路设计与验证等。求解SAT问题的算法主要分为两类：完备算法和不完备算法。尽管不完备算法可快速求解，却不能证明问题是不可满足的。完备算法不仅能在问题的属性是可满足时给出问题的解，而且在问题无解时可以给出一个完备的证明，证明此问题是不可满足的。现实生活中许多实际应用问题需要证明问题的无解，因此本文主要介绍完备算法的相关内容。

当前主流的SAT完备求解算法几乎都是基于DPLL（Davis Putnam Longmann Loveland）算法[2]衍生而来，DPLL算法主要利用单文字规则、纯文字规则和分裂规则，通过深度优先搜索二叉树，求解子句集，但是由于SAT问题的特殊性，导致DPLL算法在最坏情况下具有以问题规模为指数的时间复杂性。……