سال انتشار: ۱۳۸۶

محل انتشار: سی و هشتمین کنفرانس ریاضی ایران

تعداد صفحات: ۳

نویسنده(ها):

MOHAMMAD GHASEM ZADEH – Department of Computer, University of yazd
CHRISTOPH MEINEL – Hasso Plattner Institute, University of potsdam

چکیده:

Almost all existing Qsat solvers only accept QBFs represented in prenex-CNF. Therefore, they are required to transform the obtained formula into prenex-CNF befor launching it to a QSAT solver. This task usually cannot be done efficiently. In this paper we show haw Zero-Suppressed Binary Decision Diagram (abbreviated by ZBDD or ZDD) can be used to represent QBFs given in prenex-NNF and evaluate them efficiently. Transforming a QBF into its equivalent in prenex-NNF usually can be done efficiently.