Message passing algorithm for solving QBF using more reasoning (Q460215)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Message passing algorithm for solving QBF using more reasoning |
scientific article |
Statements
Message passing algorithm for solving QBF using more reasoning (English)
0 references
13 October 2014
0 references
Summary: 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.
0 references