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...

• Type: Conference
• Year: 2004
• Where: AUSAI
• Authors: Mohammad GhasemZadeh, Volker Klotz, Christoph Meinel
• Keywords: Artificial Intelligence, Artificial Intelligence Subjects, AUSAI 2004, Boolean Formulas, DPLL Algorithm