A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoization

Quantified Boolean formulas (QBFs) play an important role in theoretical computer science. QBF extends propositional logic in such a way that many advanced forms of reasoning can be easily formulated and evaluated. In this dissertation we present our ZQSAT, which is an algorithm for evaluating quantified Boolean formulas. ZQSAT is based on ZBDD: Zero-Suppressed Binary Decision Diagram , which is a variant of BDD, and an adopted version of the DPLL algorithm. It has been implemented in C using the CUDD: Colorado University Decision Diagram package. The capability of ZBDDs in storing sets of subsets efficiently enabled us to store the clauses of a QBF very compactly and let us to embed the notion of memoization to the DPLL algorithm. These points 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 a little overheads. ZQSAT can solve some sets of standard QBF benchmark problems (known to be hard for DPLL based algorithms) faster than the best existing solvers. In addition to prenex-CNF, ZQSAT accepts prenex-NNF formulas. We show and prove how this capability can be exponentially beneficial.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Potsdam

Year

2005

Author dc:creator

• Ghasemzadeh, Mohammad

Contributors dc:contributor

• Meinel, Christoph

• DPLL
• Zero-Suppressed Binary Decision Diagram (ZDD)
• Formeln der quantifizierten Aussagenlogik
• Erfüllbarkeit einer Formel der Aussagenlogik
• ZQSA
• Quantified Boolean Formula (QBF)
• Satisfiability
• ZQSAT

Repository record source_url

https://publishup.uni-potsdam.de/frontdoor/index/index/docId/563

OAI identifier oai:identifier

oai:kobv.de-opus4-uni-potsdam:563