一种基于消解的变量极小不可满足子公式的提取方法  

A Resolution-Based Approach for Extracting Variable Minimal Unsatisfiable Sub-Formulas

作　　者：陈振宇[1] 徐宝文[1] 周从华[2] 

机构地区：[1]东南大学计算机科学与工程学院,南京210096 [2]江苏大学计算机科学与通信工程学院,镇江212013

出　　处：《计算机研究与发展》2008年第z1期43-47,共5页Journal of Computer Research and Development

基　　金：国家杰出青年科学基金项目(60425206);国家自然科学基金项目(60403016);江苏省自然科学基金项目(BK2005060);江苏省博士后科研资助计划基金项目(0701003B)

摘　　要：变量极小不可满足(VMU)问题是极小不可满足(MU)问题的一个扩充和延伸.着重研究VMU子公式的提取算法.首先从理论上比较MU和VMU的基本性质,并分析了目前流行的MU子公式提取算法.研究Davis-Putman-消解的基本性质,给出一个判定变量极小不可满足公式的充分必要条件,进而提出一个基于消解的VMU子公式提取算法.此算法可以使用ZBDDs压缩存储消解式,并实现单步多重消解.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 step.

关 键 词：可满足问题 极小不可满足 变量极小不可满足 

分 类 号：TP331[自动化与计算机技术—计算机系统结构]