Sciweavers

Share
AUSAI
2004
Springer

Embedding Memoization to the Semantic Tree Search for Deciding QBFs

10 years 7 months ago
Embedding Memoization to the Semantic Tree Search for Deciding QBFs
Abstract. Quantified Boolean formulas (QBFs) play an important role in artificial intelligence subjects, specially in planning, knowledge representation and reasoning [20]. In this paper we present ZQSAT (sibling of our FZQSAT [15]), which is an algorithm for evaluating quantified Boolean formulas. QBF is a language that extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. ZQSAT is based on ZDD, which is a variant of BDD, and an adopted version of the DPLL algorithm. The program has been implemented in C using the CUDD package. The capability of ZDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and led us to implement the search algorithm in such a way that we could store and reuse the results of all previously solved subformulas with few overheads. This idea along some other techniques, enabled ZQSAT to solve some standard QBF benchmark problems faster than the best...
Mohammad GhasemZadeh, Volker Klotz, Christoph Mein
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where AUSAI
Authors Mohammad GhasemZadeh, Volker Klotz, Christoph Meinel
Comments (0)
books