کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6853145 658310 2016 25 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Solving QBF with counterexample guided refinement
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر هوش مصنوعی
پیش نمایش صفحه اول مقاله
Solving QBF with counterexample guided refinement
چکیده انگلیسی
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
نویسندگان
, , , ,