结合高级正向推理过程的可满足性问题解决器

摘要：

提出了一个可满足性问题解决器,它结合了DPLL(Davis Putnam Loge- mann and Loveland)算法和作为高级推理技术之一的失败性文字检查(FLD,Failed Literal Detection)技术.在失败性文字检查技术中,又提出了动态筛选方法,它包含了两条规则: 内部和外部筛选.在保证能在每个决策层上发现大部分失败性文字的同时,降低了失败性文字检查所测试的文字数目及相应的计算时间.不同于其他类型的预定义的删除标准,在这一方法中文字的删除是动态的,从这点上讲,文中的失败性文字检查算法可以适应不同类型的测试基准实例.许多不必要的测试可以被避免,因而提高了失败性文字检查的计算速度.为了进一步提高失败性文字检查的效率,故此还增加了其他静态的测试约束.实验表明,经过优化后的失败性文字检查算法的效率明显高于其他的高级正向推理技术.

关键词：可满足性问题、形式验证、电子设计自动化

所属期刊栏目：35

分类号：TP1(自动化基础理论)

资助基金：国家自然科学基金90207002,60176017;国家高技术研究发展计划863计划2002AA1Z1460,2002AA1Z1340;美国国家自然科学基金CCR-0098275,CCR-0306298

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

页数：共13页

页码：426-438