|
|||||
|
|
| 极小布尔不可满足子式的提取算法 | |
| 引用本文： | 邵明,李光辉,李晓维.极小布尔不可满足子式的提取算法[J].计算机辅助设计与图形学学报,2004,16(11):1542-1546. |
| 作者姓名： | 邵明 李光辉 李晓维 |
| 作者单位： | 1. 中国科学院计算技术研究所信息网络室,北京,100080;中国科学院研究生院,北京,100039 2. 中国科学院计算技术研究所信息网络室,北京,100080;中国科学院研究生院,北京,100039;浙江林学院信息系,杭州,311300 3. 中国科学院计算技术研究所信息网络室,北京,100080 |
| 基金项目： | 国家自然科学基金 ( 90 2 0 70 0 2,60 2 42 0 0 1)，北京市科技重点项目 ( 0 2 0 12 0 12 0 13 0 )资助 |
| 摘 要： | 研究了极小布尔不可满足子式的提取算法，它分为近似算法和精确算法两种．文中就精确算法提出了局部预先赋值的优化方案，并且在理论上证明了该算法的正确性；通过实验显示了此算法可以获得更高的效率．通过模拟实验观察到，利用完法计算法进行近似提取的一个有趣现象，即随着公式密度的增加，算法的提取误差会趋于下降． |
| 关 键 词： | 形式验证 布尔可满足问题 极小布尔不可满足子式 |
Algorithms for Extracting Minimal Unsatisfiable Boolean Sub-formula |
|
| Shao Ming , Li Guanghui , Li Xiaowei.Algorithms for Extracting Minimal Unsatisfiable Boolean Sub-formula[J].Journal of Computer-Aided Design & Computer Graphics,2004,16(11):1542-1546. | |
| Authors: | Shao Ming Li Guanghui Li Xiaowei |
| Affiliation: | Shao Ming 1,2) Li Guanghui 1,2,3) Li Xiaowei 1) 1) |
| Abstract: | The paper is concerned with the algorithms for extraction of minimal unsatisfiable (MU) Boolean sub-formula The algorithms include approximate and exact methods We propose a method of pre-assignment for exact algorithm of traversing clauses, and the correctness is proved in theory Furthermore, the experiments demonstrated the efficiency of pre-assignment method Moreover, an observation revealed that the interesting phenomenon occurs in the simulating experiments on approximate method based on complete algorithm, with the increasing density of the formula, the average error of the extraction is decreasing |
| Keywords: | formal verification Boolean satisfiability problem minimal unsatisfiable sub-formulas |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |