کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6876055 | 690199 | 2015 | 18 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Expansion-based QBF solving versus Q-resolution
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Expansion-based QBF solving versus Q-resolution Expansion-based QBF solving versus Q-resolution](/preview/png/6876055.png)
چکیده انگلیسی
This article introduces and studies a proof system âExp+Res that enables us to refute quantified Boolean formulas (QBFs). The system âExp+Res operates in two stages: it expands all universal variables through conjunctions and refutes the result by propositional resolution. This approach contrasts with the Q-resolution calculus, which enables refuting QBFs by rules similar to propositional resolution. In practice, Q-resolution enables producing proofs from conflict-driven DPLL-based QBF solvers. The system âExp+Res can on the other hand certify certain expansion-based solvers. So a natural question is to ask which of the systems, Q-resolution and âExp+Res, is more powerful? The article gives several partial responses to this question. On the positive side, we show that âExp+Res can p-simulate tree Q-resolution. On the negative side, we show that âExp+Res does not p-simulate unrestricted Q-resolution. In the favor of âExp+Res we show that âExp+Res is more powerful than a certain fragment of Q-resolution, which is important for DPLL-based QBF solving.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 577, 27 April 2015, Pages 25-42
Journal: Theoretical Computer Science - Volume 577, 27 April 2015, Pages 25-42
نویسندگان
MikoláÅ¡ Janota, Joao Marques-Silva,