Summary: Disjunctive Logic Programming (DLP), also called answer set programming, 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}_{2}^{\text{P}} =\text{NP}^{\text{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 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.