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

摘要：

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

关键词：形式验证、布尔可满足问题、极小布尔不可满足子式

所属期刊栏目：16

分类号：TP331(计算技术、计算机技术)

资助基金：国家自然科学基金9020700260242001;北京市科研项目020120120130

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

页数：共5页

页码：1542-1546