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-ﬁnding 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 deﬁne 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 Sigma_2^P e Pi_2^P. 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.
Look-Back Techniques and Heuristics in DLV: Implementation, Evaluation and Comparison to QBF Solvers / MARATEA M; RICCA F; FABER W; LEONE N. - In: JOURNAL OF ALGORITHMS. - ISSN 0196-6774. - 63:1-3(2008), pp. 70-89.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Look-Back Techniques and Heuristics in DLV: Implementation, Evaluation and Comparison to QBF Solvers|
|Data di pubblicazione:||2008|
|Citazione:||Look-Back Techniques and Heuristics in DLV: Implementation, Evaluation and Comparison to QBF Solvers / MARATEA M; RICCA F; FABER W; LEONE N. - In: JOURNAL OF ALGORITHMS. - ISSN 0196-6774. - 63:1-3(2008), pp. 70-89.|
|Appare nelle tipologie:||1.1 Articolo in rivista|