Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:
Academic
Publications
FZQSAT: A QSAT Solver for QBFs in Prenex NNF (A Useful Tool for Circuit Verification)
Edit
FZQSAT: A QSAT Solver for QBFs in Prenex NNF (A Useful Tool for Circuit Verification)  
BibTex | RIS | RefWorks Download
In this paper we present FZQSAT, which is an algo- rithm for evaluating quantified Boolean formulas presented in negation normal form (NNF). QBF is a language that ex- tends propositional logic in such a way that many advanced forms of verification, such as bounded model checking, can be easily formulated and evaluated. FZQSAT is based on ZDD which is a variant of BDD, and is an adopted version of the DPLL algorithm. 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. This idea which we call it 'em- bedding memorization to the semantic tree method in decid- ing QBFs) along some other techniques, specially the possi- bility of accepting QBFs in their prenex NNF (instead of re- quiring to transform them to prenex CNF) enabled FZQSAT to solve the 'sequential depth of circuits' problem, which is an important problem in bounded model checking, much faster than best existing solvers. FZQSAT also accepts the standard prenex CNF formulas. It manages to solve some standard QBF benchmark problems faster than best existing QSAT solvers.
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.
Share this on | Contribute to Academic