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

• 作者: 丁敏 周电 唐璞山
• 来源期刊: 中国科学E辑
• 学科: 工学
• 关键词: 可满足性问题 形式验证 电子设计自动化
• 年，卷（期）: 2005,（4）
• 页码范围: 426-438
• 页数: 13页
• 分类号: TP1
• 字数: 8580字
• 语种: 中文
• DOI: 10.3321/j.issn:1006-9275.2005.04.007

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	丁敏	上海复旦大学微电子系专用集成电路国家重点实验室	2	21	2.0	2.0
2	唐璞山	上海复旦大学微电子系专用集成电路国家重点实验室	2	21	2.0	2.0
3	周电	上海复旦大学微电子系专用集成电路国家重点实验室	1	11	1.0	1.0