Message Passing Algorithm for Solving QBF Using More Reasoning

Message Passing Algorithm for Solving QBF Using More Reasoning
复制标题

使用更多推理解决 QBF 的消息传递算法

DOI:
10.1155/2013/165927
复制
发表时间:
2013-10
影响因子:
--
通讯作者:
Zhou Junping
Zhou Junping
中科院分区:
工程技术4区
文献类型:
--
作者:
Su Weihua;Yin Minghao;Wang Jianan;Zhou Junping

文献摘要

参考文献

相似文献

我们提出了一种新颖的求解器来解决量化布尔公式问题(QBF)。为了提高性能,我们在求解QBF的消息传递算法中引入了一些推理规则。在预处理公式时,求解器结合了等式约简和超二元解析。此外,求解器在选择分支时采用消息传递方法来获取更多信息。通过使用单元传播、冲突驱动学习以及可满足性定向暗示和学习,求解器处理分支。实验结果还表明该求解器能够有效地求解QBF问题。
We present a novel solver for solving Quantified Boolean Formulae problem (QBF). In order to improve the performance, we introduce some reasoning rules into the message passing algorithm for solving QBF. When preprocessing the formulae, the solver incorporates the equality reduction and the hyperbinary resolution. Further, the solver employs the message passing method to obtain more information when selecting branches. By using the unit propagation, conflict driven learning, and satisfiability directed implication and learning, the solver handles the branches. The experimental results also show that the solver can solve QBF problem efficiently.
DOI: 10.1126/science.1073287
发表时间: 2002-08-02
期刊: SCIENCE
影响因子: 56.9
作者:
Mézard, M;Parisi, G;Zecchina, R
通讯作者: Zecchina, R
DOI: 10.1007/3-540-45744-5_27
发表时间: 2001-06
期刊: --
影响因子: --
作者:
E. Giunchiglia;Massimo Narizzano;A. Tacchella
通讯作者: E. Giunchiglia;Massimo Narizzano;A. Tacchella
DOI: 10.1007/978-3-540-24605-3_3
发表时间: 2003-05
期刊: --
影响因子: --
作者:
Ian P. Gent;E. Giunchiglia;Massimo Narizzano;Andrew Rowley;A. Tacchella
通讯作者: Ian P. Gent;E. Giunchiglia;Massimo Narizzano;Andrew Rowley;A. Tacchella
DOI: --
发表时间: 2000-07
期刊: --
影响因子: --
作者:
Uwe Egly;Thomas Eiter;H. Tompits;S. Woltran
通讯作者: Uwe Egly;Thomas Eiter;H. Tompits;S. Woltran
DOI: 10.1007/3-540-46135-3_14
发表时间: 2002-09
期刊: --
影响因子: --
作者:
Lintao Zhang;S. Malik
通讯作者: Lintao Zhang;S. Malik