使用SAT求解器产生所有极小冲突部件集

来源 :电子学报 | 被引量 : 0次 | 上传用户:liongliong549
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效
其他文献
采用RACE技术,从茶树新品系“1005”的嫩芽中克隆出ANR基因的全长cDNA(1260bp),其推导的氨基酸序列与茶树、葡萄花色素还原酶的一致性分别为99%和84%;并成功构建了ANR基因的原核表达
运输企业与普通企业存在一定差异,在其成长的同时,由于本身存在的局限性,以及在外部环境共同作用下,存在着自身发展和市场经济发展不协调的现象。通过分析运输企业内部财务管
随着大陆经济蓬勃发展,越来越多外籍企业也随之进驻参与竞争,不仅带来了众多外籍员工,本地企业也因为要往国际舞台拓展招募了不少外籍员工,以吸收相关的国际经验。微软大中华区的
本文主要阐述食品药品检测实验室的质量监督,目的是提高食品药品检测实验室对质量监督工作的重视程度,促进质量管理体系的持续改进。本文从质量监督的内容、质量监督的实施和
近年来,随着社会经济的不断发展与社会对人才需求的变化,对高职院校的学生也提出了更多新的要求。而随着各类思想潮流的涌入,也使高职院校学生的思想政治教育工作出现了一些
为了更好地做好档案管理工作,在信息化大背景下,需要在档案管理工作各个环节实现计算机化,通过各学科和不同专业的知识,各个部门相互配合,然后采取有针对性的措施来提高机关
应用4种分布函数对6个垦复糙花少穗竹林样地全部立竹及其各龄级的秆径分布进行拟合,并以1个未垦复样地为对比,结果表明,各样地拟合效果最好的均是Weibull分布.垦复样地的立竹总
如果女性把同样的模式应用于对待手头的工作,则其工作的理性水平、在反省总结中的进步水平将非常突出。
本试验在农业部甘蔗生理生态与遗传改良重点开放实验室建立的甘蔗再生体系的基础上,在甘蔗愈伤组织培养的不同阶段,分别加入不同质量浓度的G418选择性试剂,以确定用于甘蔗遗传转
采用ZAP Express cDNA Gigapack Ⅲ Gold Cloning Kit试剂盒,构建了小菜蛾(Plutella xylostella)的全长cDNA文库.利用TRIzol试剂盒提取小菜蛾成虫总mRNA,通过Oligo试剂将mRNA反