We introduce a novel algorithm for the evaluation of quantified boolean formulas (QBFs), which we call sKizzo. Our work is firstly framed in the broad field of algorithms for automated deduction. Then, we enlighten the strong application-related interest in decision procedures for QBFs. The algorithm itself is thoroughly discussed. It integrates within a uniform framework several different ideas and techniques: classical resolution-based QBF reasoning, algorithms for structure reconstruction, propositional skolemization, BDD-based representations, symbolic reasoning, search-based decision procedures, compilation to SAT techniques, and more. A detailed account of each module in the solver is presented, together with the overall architecture explaining how they interact with one another. We also report of our first implementation for the algorithm. It was used to experimentally evaluate our approach, yielding very interesting results. The related literature is carefully reviewed, aiming to point out the many distinguishing features of sKizzo. Finally, a large section is devoted to the presentation of our ongoing efforts and future work on the topic
sKizzo: A Suite to Evaluate and Certify QBFs
Benedetti, Marco
2004-01-01
Abstract
We introduce a novel algorithm for the evaluation of quantified boolean formulas (QBFs), which we call sKizzo. Our work is firstly framed in the broad field of algorithms for automated deduction. Then, we enlighten the strong application-related interest in decision procedures for QBFs. The algorithm itself is thoroughly discussed. It integrates within a uniform framework several different ideas and techniques: classical resolution-based QBF reasoning, algorithms for structure reconstruction, propositional skolemization, BDD-based representations, symbolic reasoning, search-based decision procedures, compilation to SAT techniques, and more. A detailed account of each module in the solver is presented, together with the overall architecture explaining how they interact with one another. We also report of our first implementation for the algorithm. It was used to experimentally evaluate our approach, yielding very interesting results. The related literature is carefully reviewed, aiming to point out the many distinguishing features of sKizzo. Finally, a large section is devoted to the presentation of our ongoing efforts and future work on the topicI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
