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 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.