SAT问题研究小结预备知识：1基于模型诊断的基本概念介绍：首先我们介绍基于模型诊断的主要思想和框架结构：
基本定义：（1）诊断系统：一个诊断系统符号化定义即为一个三元组SDCOMPSOBS其中SD为系统描述，是一阶谓词公式集合；COMPS是系统的组成部件集合，是一个有限常量集合，而OBS是一个观测集合，是一阶谓词公式的有限集合。简而言之就是把一个相关的系统抽象成符号化的几个部分，然后把系统模型化，根据逻辑关系和相关的硬件结构抽象成模型，根据模型推理出系统正常的输出，而往往在实际系统中得到的观测和预期的结果不符，此时便需要诊断出哪些元件可能出现故障，出现故障的原因，并找到故障元件并解决，其中最主要的是故障元件集合的找出即：诊断集合。（2）我们把一个元件不正常工作符号化表示即为：ABc”ab
ormal”ABc为真当且仅当c反常，其中cCOMPS。（3）基于一致性诊断：设组件集合COMPS，称为关于SDCOMPSOBS的一个基于一致性诊断，如果
SDOBSABccCOMPS是可满足的。
（4）极小诊断集：称一个关于SDCOMPSOBS的一个基于一致性诊断是极小的MCBDif不存在的任何真子集也是关于SDCOMPSOBS的一个基于一致性诊断。（5）由此我们可以知道：要想判断一个诊断集合是否是基于一致性诊断，只需要判断在这个诊断集合中的组件都是反常的是故障的，然后剩下的组件工作正常工作和系统的相关描述以及系统在这种情况下系统的观测是否逻辑上可以解释的。（6）命题可满足性问题propositio
alSatisfiabilityProblemSAT是人工智能里的一个分支，它是完全NP问题，并且人工智能中很多的NP问题都可以转化成SAT问题，然后求解，相应的基于模型诊断问题MBD问题也可转化为SAT问题，然后求解。（7）集成组合电路可以转化CNF例如与门电路：
f其可转化为abc如果与门工作正常的情况下：则有：
c
c
，其转化过程如下：ab
cababccabcababccababccababc化简转化即为：cacbabc
同理其它组合电路门转化为CNF如下：
一般的组合电路如下图：
f其对应的CNF如下：
2SAT问题定义可满足问题的一些基本定义，表示如下：定义21文字literal对于变量集合Xx1x2x3x
文字li是变量xi或者否定xi。定义22子句clause子句Ci是文字li的析取Cil1l2l3l4lm定义23合取范式co
ju
ctive
ormalformCNFCNFF是子句的合取r