MiniSAT求解器在电路故障诊断中的应用

曾维鹏，蔡莉莎，吴恒玉，林尔敏

(海南软件职业技术学院1.软件工工程系，2.电子工程系，海南琼海571400)

早期的电路故障诊断主要是依靠工程技术人员借助一些常规的工具对电路进行逐段查找。这不但要求技术人员对电路的连接及特性有比较深刻的了解，而且要花费大量时间。随着电路日趋复杂以及计算机的发展，已更多使用人工智能方法进行故障诊断。人工智能的故障诊断方法是指系统运行中，当系统的实际表现与系统模型的预期值不一致时，表明系统工作不正常，至少有一个元件出现了故障。此时需要进行故障诊断，并根据诊断结果为系统故障恢复提供依据。由于电路出现故障则集合内所有部件均正常工作是不可能满足的，于是将判断一个部件集是否有故障的问题非常自然地转化为可满足性问题。

1 SAT求解器

命题可满足性问题SAT(Staisfiablity)是计算机理论界与逻辑学界共同关注的一个重大问题。SAT问题具体是指，给定一个包含n个布尔变量X1，X2，…Xn(只能为真或假)的逻辑析取范式，是否存在它们的一组取值组合，使得该析取范式被满足［1，2]?

在现实世界中，很多重要且难以解决的验证和组合问题均可转化成SAT问题，因此对它的研究在理论和实践方面都非常有意义［3]。许多优秀的SAT求解器的开发，如MinSat等，使得SAT求解可以完全自动化。SAT求解器近几年得到广泛应用研究和改进，特别是在自动规划、模型诊断和电路等价性等领域。每年一度的国际SAT竞赛促使SAT求解器的效率不断提高，很多问题都可以转换成SAT求解问题。我们如能利用现有的SAT求解器，就可方便给出问题的所有答案。

使用MiniSAT求解器需先将要求解的公式等价地转换成合取范式CNF(Conjunctive Novmal Form)，合取范式是由基本和之积组成的公式，即由或与表达式组成的公式。然后以DIMACS的格式表达。每个DIMACS文件总是从p cnf＜VARIABLES＞＜CLAUSES＞开始的。其中VARIABLES表示布尔变量的个数，CLAUSES表示子句的个数。每一行都以空格和0表示一个子句的结束。用正整数表示布尔变量，该数所对应的负整数表示该布尔变量的非。

2 算法描述

可满足性算法的基本思想为:将任何一个逻辑命题转化成一个子句集，通过各种可满足性方法来判定该子句集是否可满足，从而决定该命题是否成立［4]。为了判定一个数字电路是否存在电路故障，我们将数字电路系统定义为三元组:系统描述SD，组成部件集合COMPS和观测集OBS。基于可满足性算法的基本思想，为了判定一个部件集是否存在故障，其实就是判定该部件集中所有组件的正常行为描述与相关的系统描述及观测描述是否逻辑一致。我们只需将该部件集相关的系统描述与观测描述代入SAT求解器，将判断部件集是否存在故障转换为SAT求解问题。如果可满足，SAT求解器(包括MiniSAT)得到结果判定命题公式集是真的。如果不可满足，则该部件集存在故障。

本文以全加器电路为例，介绍利用MiniSAT求解器在电路故障诊断中的应用。全加器电路如图1所示。

3 使用CNF对系统及观测建模

图1 全加器电路

MiniSAT求解器以合取范式CNF文件作为输入，每一个命题公式(集)均可以转化为一个CNF文件描述。本文使用逻辑命题对其行为建模。对于系统中每一个部件使用一个变量表示，而且所有的联结点也分别用不同的变量表示该点的取值。对于系统中的每一个部件，仅考虑每一个部件的所有可能的正常行为模型的子句表示。每一个部件的行为使用命题逻辑公式表示，将每一个命题逻辑公式等价转化为相应的子句形式。判定一个电路是否存在故障也就是要检测每一个部件正常工作时它们的所有行为是否可满足。

图1全加器中1、2、3分别表示相应的输入节点变量，4、5分别表示相应的输出节点变量，6、7、8则表示相应的内部联结点变量。此外，所含的部件变量异或门X1，X2，X3、与门A1，A2以及或门O1则分别使用9、11、10、12和13表示。

以全加器电路中X1异或门为例说明如何建立数字电路系统的系统描述SD。当异或门X1无故障时即OK(X1)，输入节点变量1、2为正值，则异或门输出为-6，其逻辑描述为:OK(X1)∧1∧2→-6，将其转换为范式的形式(将蕴含符号→去掉)变成-OK(X1)∨-1∨-2∨-6。考虑异或门不同输入所产生的不同逻辑描述，则异或门的合取范式CNF表达如下:(-OK(X1)∨-1∨-2∨-6)∧(-OK(X1)∨1∨2∨-6)∧(-OK(X1)∨-1∨2∨6)∧(-OK(X1)∨1∨-2∨6)。9-13表示各相应部件的正常谓语，取正值分别表示各部件正常工作;如9表示OK(X1)。因此异或门的合取范式CNF也可以表达如下:(-9∨-1∨-2∨-6)∧(-9∨1∨2∨-6)∧(-9∨-1∨2∨6)∧(-9∨1∨-2∨6)。

全加器电路中其他的门电路同理可求。于是全加器电路系统描述的CNF表达可以写成:

4 调用SAT求解器

MiniSAT求解器是在Linux环境下运行的。首先新建一个名为2的文本文档，里面是全加器系统描述、组件正常行为描述以及观测的CNF文件，如图2所示。

图2 全加器系统描述以及观测的CNF文件

其次输入指令为./minisat 22relt调用MiniSAT求解器判定CNF文件的可满足性，判定的结果在2relt文本文档中，如图3所示。

图3 MiniSAT求解器求解结果

图中，第一行输出SAT，则表示输入结果可满足，第二行则是满足表达式的布尔变量值的集合，即当异或门X1，X2，与门A1，A2无故障且输入节点变量为-1，-2，-3，全加器输出结果为-4，-5时，整个命题集是可满足的。当输出结果是可满足时，第二行则显示是满足表达式的布尔变量值的其中一个集合。如果想得到其他解，可以添加一个子句，将已有解作为增加的子句建立新的输入，将新的CNF文件放到文件second.in中，然后运行:./minisat second.in second.out。反复如此，直至求解出满足表达式的布尔变量值的所有集合。而如果输入其他使整个命题不可满足的观测集时，如输入观测集OBS为-10，-20，-30，40，-50时，使用MiniSAT求解器求解的结果为UNSAT表示整个电路命题不可满足，全加器电路存在故障。

5 结语

通过将查找数字电路故障问题转换为SAT求解问题，我们可以通过将复杂的逻辑推理题转换成命题逻辑的SAT问题，并通过MiniSAT求解器自动解答。基于SAT的运算电路查错方法，自动化程度高，能处理大规模的运算电路，有较强的查找错误的能力［5]。

［1] Cook S A.The complexity of theorem-proving procedures［C] .New York:Proceedings of the third ACM Symposium on Theory of Computing，1971:151-158.

［2] Crawford J M，Auton L D.Experimental results on the crossover point in satisfability problems［C] .California:Proc.of AAA193.Aug1993:21-27.

［3] 田聪，段振华，王小兵.Einstein谜的SAT求解［J] .重庆:计算机科学，2010，37(5):184-185.

［4] 赵相福，欧阳丹彤.使用SAT求解器产生所有极小冲突部件集［J] .北京:电子学报，2009，37(4):804-810.

［5] 陈云霁，张健，沈海华，胡伟武.一种基于SAT的运算电路查错方法［J] .北京:计算机学报，2007，30(12):2082-2089.