کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6853145 | 658310 | 2016 | 25 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Solving QBF with counterexample guided refinement
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
This article puts forward the application of Counterexample Guided ion Refinement (CEGAR) in solving the well-known PSPACE-complete problem of quantified Boolean formulas (QBF). The article studies the application of CEGAR in two scenarios. In the first scenario, CEGAR is used to expand quantifiers of the formula and subsequently a satisfiability (SAT) solver is applied. First it is shown how to do that for two levels of quantification and then it is generalized for arbitrary number of levels by recursion. It is also shown that these ideas can be generalized to non-prenex and non-CNF QBF solvers. In the second scenario, CEGAR is employed as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of benchmark families and that the DPLL solver benefits from the additional type of learning.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Artificial Intelligence - Volume 234, May 2016, Pages 1-25
Journal: Artificial Intelligence - Volume 234, May 2016, Pages 1-25
نویسندگان
MikoláÅ¡ Janota, William Klieber, Joao Marques-Silva, Edmund Clarke,