ACCEPTING MORE GENERAL FORMS OF QBFS
محل انتشار: سی و هشتمین کنفرانس ریاضی ایران
سال انتشار: 1386
نوع سند: مقاله کنفرانسی
زبان: انگلیسی
مشاهده: 1,461
متن کامل این مقاله منتشر نشده است و فقط به صورت چکیده یا چکیده مبسوط در پایگاه موجود می باشد.
توضیح: معمولا کلیه مقالاتی که کمتر از ۵ صفحه باشند در پایگاه سیویلیکا اصل مقاله (فول تکست) محسوب نمی شوند و فقط کاربران عضو بدون کسر اعتبار می توانند فایل آنها را دریافت نمایند.
- صدور گواهی نمایه سازی
- من نویسنده این مقاله هستم
استخراج به نرم افزارهای پژوهشی:
شناسه ملی سند علمی:
AIMC38_258
تاریخ نمایه سازی: 28 مرداد 1387
چکیده مقاله:
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.
کلیدواژه ها:
Quantified Boolean Formula (QBF) ، Zero-Suppressed Binary Decision Diagram (ZDD) ، Satisfiability ، QSAT ، Negation Normal From (NNF)
نویسندگان
MOHAMMAD GHASEM ZADEH
Department of Computer, University of yazd
CHRISTOPH MEINEL
Hasso Plattner Institute, University of potsdam