On Look-Ahead Heuristics in Disjunctive Logic Programming

Disjunctive logic programming (DLP), also called answer set programming (ASP), is a convenient programming paradigm which allows for solving problems in a simple and highly declarative way. The language of DLP is very expressive and able to represent even problems of high complexity (every problem in the complexity class Sigma(P)(2) = NP(NP). During the last decade, efficient systems supporting DLP have become available. Virtually all of these systems internally rely on variants of the Davis-Putnam procedure (for deciding propositional satisfiability [SAT]), combined with a suitable model checker. The heuristic for the selection of the branching literal (i.e., the criterion determining the literal to be assumed true at a given stage of the computation) dramatically affects the performance of a DLP system. While heuristics for SAT have received a fair deal of research, only little work on heuristics for DLP has been done so far. In this paper, we design, implement, optimize, and experiment with a number of heuristics for DLP. We focus on different look-ahead heuristics, also called "dynamic heuristics" (the DLP equivalent of unit propagation [UP] heuristics for SAT). These are branching rules where the heuristic value of a literal Q depends on the result of taking Q true and computing its consequences. We motivate and formally define a number of look-ahead heuristics for DLP programs. Furthermore, since look-ahead heuristics are computationally expensive, we design two techniques for optimizing the burden of their computation. We implement all the proposed heuristics and optimization techniques in DLV-the state-of-the-art implementation of disjunctive logic programming, and we carry out experiments, thoroughly comparing the heuristics and optimization techniques on a large number of instances of well-known benchmark problems. The results of these experiments are very interesting, showing that the proposed techniques significantly improve the performance of the DLV system.