Heuristic Survey Propagation Algorithm for Solving QBF Problem
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    This paper presents a heuristic survey propagation algorithm for solving Quantified Boolean Formulae (QBF) problem. A QBF solver based on the algorithm is designed, namely HSPQBF (heuristic survey propagation algorithm for solving QBF). This solver is a QBF reasoning engine that incorporates Survey Propagation method for problem solving. Using the information obtained from the survey propagation procedure, HSPQBF can select a branch accurately. Furthermore, when handling the branches, HSPQBF uses efficient technology to solve QBF problems, such as unit propagation, conflict driven learning, and satisfiability directed at implication and learning. The experimental results also show that HSPQBF can solve both random and QBF benchmark problems efficiently, which validates the effect of using survey propagation in a QBF solving process.

    Reference
    Related
    Cited by
Get Citation

殷明浩,周俊萍,孙吉贵,谷文祥.求解QBF 问题的启发式调查传播算法.软件学报,2011,22(7):1538-1550

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 18,2008
  • Revised:March 29,2010
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063