SAT问题求解.doc

SAT问题研究小结 预备知识： 基于模型诊断的基本概念介绍： 首先我们介绍基于模型诊断的主要思想和框架结构： 基本定义： 诊断系统： 一个诊断系统符号化定义即为一个三元组(SD,COMPS,OBS),其中SD为系统描述，是一阶谓词公式集合；COMPS是系统的组成部件集合，是一个有限常量集合，而OBS是一个观测集合，是一阶谓词公式的有限集合。简而言之就是把一个相关的系统抽象成符号化的几个部分，然后把系统模型化，根据逻辑关系和相关的硬件结构抽象成模型，根据模型推理出系统正常的输出，而往往在实际系统中得到的观测和预期的结果不符，此时便需要诊断出哪些元件可能出现故障，出现故障的原因，并找到故障元件并解决，其中最主要的是故障元件集合的找出即：诊断集合。 我们把一个元件不正常工作符号化表示即为： AB(c):”abnormal”,AB(c)为真当且仅当c反常，其中cCOMPS。 基于一致性诊断： 设组件集合，称为关于(SD,COMPS,OBS)的一个基于一致性诊断，如果是可满足的。 极小诊断集： 称一个关于(SD,COMPS,OBS)的一个基于一致性诊断是极小的(MCBD),if 不存在的任何真子集也是关于(SD,COMPS,OBS)的一个基于一致性诊断。 由此我们可以知道：要想判断一个诊断集合是否是基于一致性诊断，只需要判断在这个诊断集合中的组件都是反常的(是故障的)，然后剩下的组件工作正常工作和系统的相关描述以及系统在这种情况下系统的观测是否逻辑上可以解释的。 命题可满足性问题(propositional Satisfiability Problem,SAT)是人工智能里的一个分支，它是完全NP问题，并且人工智能中很多的NP问题都可以转化成SAT问题，然后求解，相应的基于模型诊断问题(MBD)问题也可转化为SAT问题，然后求解。 集成组合电路可以转化CNF 例如与门电路： 其可转化为()，其转化过程如下： 如果与门工作正常的情况下： 则有： 同理其它组合电路门转化为CNF如下： 一般的组合电路如下图： 其对应的CNF如下： SAT问题定义 可满足问题的一些基本定义，表示如下： 定义2.1 文字(literal):对于变量集合X={x1,x2,x3,....,xn},文字li是变量xi或者否定-xi。 定义2.2 子句(clause): 子句Ci是文字li的析取,. 定义2.3. 合取范式(conjunctive normal form,CNF):CNF F是子句的合取， . 定义2.4 赋值(assignment):v:X{0,u,1},对于变量集合{x1,x2,x3,x4,...,xn}: (1)完全赋值(complete assignment):v(x){0,1},对于所有的xX; (2)部分赋值(partial assignment):v(x){0,u,1},其中u是自由变量，其取值范围为：0u1,对于所有的xX; (3)对于给定的一个CNF F,SAT(F)=1,如果存在一组赋值v,使v(F)=1,类似的，对于所有的x完全赋值v,v(F)=0,此时SAT(F)=0. SAT问题一般描述为：对于N个布尔变量X={x1,x2,x3,....,xn},找到变量的一组赋值，满足在CNF中的每个子句都至少有一个文字取真，并且这组赋值能使所有的子句都能取真。若找到这样一组赋值，则称该SAT问题是可满足的(SAT),如果没有任何一组变量赋值，使得SAT可满足，则称该SAT问题是不可满足的(UNSAT). 例如 CNF F1：,则F1找到一组赋值x1=1,x2=0,x3=1使得F1=1，那么该SAT问题是可满足的，而CNF F2：，F2就找不到一组赋值，使得F2=1,所以该SAT问题是不可满足的。 SAT求解器可以通过接收一个CNF描述文件调用完备算法或者不完备算法来求得这个CNF描述文件的可满足和不可满足。在其中任何的命题公式都可以转化为CNF描述文件。CNF描述文件的格式，如下： P cnf 2 3 //CNF描述文件的语法,”p cnf”是关键字;”2”代表变量的个数,”3”代表子句的个数; 1 0 //”1”和”-1”是文字，表示变量和变量的否定,即文字; -1 -2 0 //每一行代表一个子句，并以”0”作为子句结束表示。 2 0 任何的一个命题公式也都可以通过变形，转化为CNF描述文件，例如 R={-AB,BA,-C,-A},可以表示为CNF描述文件为： P cnf 3 4 1 2 0 -2 3 0 -3 0 -1 0 我们要想验证R是否是