极小布尔不可满足子式的提取算法

• 作者: 李光辉 李晓维 邵明
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 形式验证 布尔可满足问题 极小布尔不可满足子式
• 年，卷（期）: 2004,（11）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 1542-1546
• 页数: 5页
• 分类号: TP331
• 字数: 5042字
• 语种: 中文
• DOI: 10.3321/j.issn:1003-9775.2004.11.013

摘要

研究了极小布尔不可满足子式的提取算法,它分为近似算法和精确算法两种 .文中就精确算法提出了局部预先赋值的优化方案,并且在理论上证明了该算法的正确性;通过实验显示了此算法可以获得更高的效率 .通过模拟实验观察到,利用完全算法进行近似提取的一个有趣现象,即随着公式密度的增加,算法的提取误差会趋于下降.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李晓维	中国科学院计算技术研究所信息网络室	127	1467	20.0	32.0
2	邵明	中国科学院计算技术研究所信息网络室	36	161	8.0	11.0
6	李光辉	中国科学院计算技术研究所信息网络室	17	172	9.0	13.0