| 一种基于消解的变量极小不可满足子公式的提取方法 |
| |
| 引用本文： | 陈振宇,徐宝文,周从华. 一种基于消解的变量极小不可满足子公式的提取方法[J]. 计算机研究与发展, 2008, 45(Z1): 43-47 |
| |
| 作者姓名： | 陈振宇 徐宝文 周从华 |
| |
| 作者单位： | 1. 东南大学计算机科学与工程学院,南京,210096
2. 江苏大学计算机科学与通信工程学院,镇江,212013 |
| |
| 基金项目： | 国家自然科学基金 , 国家自然科学基金 , 江苏省自然科学基金 , 江苏省博士后科学基金 |
| |
| 摘 要： | 变量极小不可满足(VMU)问题是极小不可满足(MU)问题的一个扩充和延伸.着重研究VMU子公式的提取算法.首先从理论上比较MU和VMU的基本性质,并分析了目前流行的MU子公式提取算法.研究Davis-Putman-消解的基本性质,给出一个判定变量极小不可满足公式的充分必要条件,进而提出一个基于消解的VMU子公式提取算法.此算法可以使用ZBDDs压缩存储消解式,并实现单步多重消解.
|
| 关 键 词： | 可满足问题 极小不可满足 变量极小不可满足 |
| 修稿时间： | 2007-07-10 |
A Resolution-Based Approach for Extracting Variable Minimal Unsatisfiable Sub-Formulas |
| |
| Chen Zhenyu,Xu Baowen,Zhou Conghua. A Resolution-Based Approach for Extracting Variable Minimal Unsatisfiable Sub-Formulas[J]. Journal of Computer Research and Development, 2008, 45(Z1): 43-47 |
| |
| Authors: | Chen Zhenyu Xu Baowen Zhou Conghua |
| |
| Affiliation: | Chen Zhenyu1,Xu Baowen1,, Zhou Conghua21(School of Computer Science , Engineering,Southeast University,Nanjing 210096)2(School of Computer Science , Telecommunication Engineering,Jiangsu University,Zhenjiang 212013) |
| |
| Abstract: | Variable minimal unsatisfiability (VMU) is a generalization of minimal unsatisfiability (MU). This paper is concerned with the extraction algorithm of VMU sub-formulas. The properties of MU and VMU are compared. Davis-Putman-resolution is studied and a necessary and sufficient condition is given to decide VMU formulas. Furthermore, a resolution-based algorithm is presented to extract VMU sub-formulas. This approach can compactly represent formulas using ZBDDs and perform multiple resolutions in a single ste... |
| |
| Keywords: | satisfiability problem minimal unsatisfiability variable minimal unsatisfiability |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
