可满足性求解器中一种可观无关性利用方法

摘要：

为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.

关键词：可满足性、电路结构、可观无关性、控制唯一性

所属期刊栏目：21

分类号：TP391.7(计算技术、计算机技术)

资助基金：国家自然科学基金60273081

在线出版日期：2009-04-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：183-189