Solving ＃QBF Using Extension Rule

摘要：

Extension rule is a new method for computing the number of models for SAT formulae. In this paper, we investigate the use of the extension rule in solving ＃QBF, i.e., computing the number of QX... Qnxn which makes the Quantified Boolean Formulas (QBF) Q1x1... QnXnFevaluate to true. We present a ＃QBF algorithm based on the extension rule, namely QBFMC, which also integrates the unit propagation and the component analysis together. These excellent technologies improve the efficiency of solving ＃QBF problems efficiently.

关键词： extension rule unit propagation component analysis ＃QBF

作者: Junping Zhou Chunguang Zhou Yandong Zhai Yongjuan Yang

作者单位: College of Computer Science and Technology, Jilin University, Changchun 130012 China College of Computer Science, Northeast Normal University, Changchun 130117 China

会议类型: 国际会议

会议名称: 2010 International Conference on Advanced Mechanical Engineering(2010年先进机械工程国际学术会议 AME 2010)

会议地点: 洛阳

会议语种:英文

页码: 250-254

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