基于演绎长度的学习子句删除策略

常文静，徐 扬，吴贯锋

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算法在最坏情况下具有以问题规模为指数的时间复杂性。……