Paper Title:
Solving #QBF Using Extension Rule
  Abstract

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 Q1x1…Qn xn which makes the Quantified Boolean Formulas (QBF) Q1x1…Qn xnF evaluate 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.

  Info
Periodical
Edited by
Zhenyu Du and Bin Liu
Pages
250-254
DOI
10.4028/www.scientific.net/AMM.26-28.250
Citation
J. P. Zhou, C. G. Zhou, Y. D. Zhai, Y. J. Yang, "Solving #QBF Using Extension Rule", Applied Mechanics and Materials, Vols. 26-28, pp. 250-254, 2010
Online since
June 2010
Export
Price
$32.00
Share

In order to see related information, you need to Login.

In order to see related information, you need to Login.

Authors: Jun Ping Zhou, Chun Guang Zhou, Ming Hao Yin, Hui Yang
Abstract:Extension rule is a new method for computing the number of models for a given propositional formula. In some sense, it is actually an inverse...
268
Authors: Qin Guo, Ai Lian Wang, Ying Liu
Abstract:Preprocessing model counting instances can reduce their size considerably and decrease the solving time. In this paper we present a...
2033
Authors: Ya Qiong Jiang, Jun Wang
Chapter 3: Information Technology for Materials
Abstract:Knowledge compilation is a common technique for propositional logic knowledge bases. A given knowledge base is transformed into a normal...
347