Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
Strengthening Semantic-tree Method in evaluating QBFs
Edit
Strengthening Semantic-tree Method in evaluating QBFs   (Citations: 1)
BibTex | RIS | RefWorks Download
The semantic-tree approach is the most robust method for deciding QBFs. This method is very similar to the DPLL algorithm for evaluating SAT instances. In this paper we show how memorization can be embedded to this method to get better results. In other words we present an algorithm for evaluating QBFs, which is based on an adopted version of semantic-tree method and ZDDs (which are variants of BDDs). The capability of ZDDs in storing sets of subsets efficiently, enabled us to store the formula very compact and led us to implement the search algorithm in such a way that we could store and reuse the results of all already solved subformulas. We call this idea: 'strengthening semantic-tree method by memorization'. This idea along some other techniques, enabled our algorithm to solve a bunch of the standard QBF benchmark problems faster than the best existing QBF solvers. Keywords: DPLL, Zero-Suppressed Binary Decision Diagram (ZDD), Quantified Boolean For- mulae (QBF), Satisfiability, QSAT, Memorization, Dynamic Programming.
Published in 2004.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Order by:

Citations (1)

Share this on | Contribute to Academic