کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
429304 687181 2008 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Look-back techniques and heuristics in DLV: Implementation, evaluation, and comparison to QBF solvers
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Look-back techniques and heuristics in DLV: Implementation, evaluation, and comparison to QBF solvers
چکیده انگلیسی

DLV is the state-of-the-art system for evaluating disjunctive answer set programs. As in most Answer Set Programming (ASP) systems, its implementation is divided in a grounding part and a propositional model-finding part. In this paper, we focus on the latter, which relies on an algorithm using backtracking search.Recently, DLV has been enhanced with backjumping techniques, which also involve a reason calculus, recording causes for the truth or falsity of atoms during the search. This reason calculus allows for looking back in the search process for identifying areas in the search space in which no answer set will be found. We can also define heuristics which make use of the information about reasons, preferring literals that were the reasons of more inconsistent branches of the search tree. This heuristics thus use information gathered earlier in the computation, and are therefore referred to as look-back heuristics.In this paper, we formulate suitable look-back heuristics and focus on the experimental evaluation of the look-back techniques that we have implemented in DLV, obtaining the system DLVLB. We have conducted a thorough experimental analysis considering both randomly-generated and structured instances of the 2QBF problem, the canonical problem for the complexity classes and . Any problem in these classes can be expressed uniformly using ASP and can therefore be solved by DLV. We have also evaluated the same benchmark using “native” QBF solvers, which were among the best solvers in recent QBF Evaluations. The comparison shows that DLV endowed with look-back techniques is competitive with the best available QBF solvers on such instances.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Algorithms - Volume 63, Issues 1–3, January–July 2008, Pages 70-89