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

摘要：

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

关键词： 布尔可满足问题 极小布尔不可满足子式 超大规模集成电路 局部预先赋值

作者: 邵明 李光辉 李晓维

作者单位: 中国科学院计算技术研究所信息网络室(北京);中国科学院研究生院(北京) 中国科学院计算技术研究所信息网络室(北京);中国科学院研究生院(北京);浙江林学院信息系(杭州) 中国科学院计算技术研究所信息网络室(北京)

会议类型: 国内会议

会议名称: 全国第13届计算机辅助设计与图形学学术会议暨全国第16届计算机科学与技术应用学术会议

会议地点: 合肥

会议语种:中文

页码: 268-271

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