论文部分内容阅读
人工智能被称为二十一世纪三大尖端技术之一，目前已深入到人们科研、工作和生活的各个领域，并在不断地发展。可满足性问题（SATisfiability, SAT）研究的兴起拉开了人工智能研究的序幕，其后SAT的研究一直是人工智能领域的核心技术和最具挑战性的研究方向之一，同时也是被公认为硕果累累的研究分支。本论文主要研究基于扩展规则的SAT求解方法，并探索如何有效地结合SAT技术提高等价性验证和不一致诊断这两类重要问题的求解效率。通过对基于扩展规则SAT方法的研究，给出了基于半扩展规则的SAT方法，进而提高问题的求解效率。此方法中当一个极大项子句可被某一子句扩展时，那么基于此子句半扩展出的所有极大项子句都不必再判断是否可由子句集中子句扩展，从而减少了需要判断的极大项子句的个数。形式化等价性验证方法取得突破性进展是基于割集方法的引入，但此方法存在误判现象。通过对现有误判方法的研究，给出结合SAT消除误判的等价性验证方法。此方法先计算不等价时对应的约束关系，然后再与模型对应的约束关系一起调用求解器消除误判。不用额外加入其它的辅助结构，适用于寄存器传输级模型(Register Transfer Level,RTL)和RTL的验证以及系统级模型(System Level Model, SLM)和RTL的验证。集成电路中不一致诊断是紧随等价性验证之后的重大研究课题和难题，通过对不一致诊断中求解问题相似性进行研究，给出了可以增量求解不一致诊断的动态半扩展规则(Dynamic Semi-Extension Rule,DSER)方法。通过对扩展规则方法中极大项空间的研究，给出了已扩展极大项空间和未扩展极大项空间概念，进而给出了动态的基于半扩展规则证明方法DSER。根据不一致诊断问题求解中一系列问题的相似性，利用本文提出的DSER方法增量求解不一致诊断问题。一次求解一系列相似的不一致诊断问题，不用对每一个子问题分别求解，极大程度地有效利用求解过程中信息。此外，为了提高不一致诊断效率，本文还给出利用标志传播的诊断方法和诊断问题中基于动态极大度的碰集计算方法。在标志传播的诊断方法中提出元件输出标志的概念，此方法通过在系统中传播输出标志，来判断元件集合是否为系统的诊断，避免了求解是否为诊断时引起的NP-完全问题;在碰集计算方法中提出未扩展元素度的概念和结点度的概念，进而按照未扩展元素度由大到小的顺序求解，极早地生成集合簇的碰集，有效地减少碰集的计算次数；并且直接根据结点度得出结点对应的集合是否为集合簇的碰集，避免计算集合是否为集合簇的碰集。