Efficient Approximation of Well-Founded Justification and Well-Founded Domination (Corrected and Extended Version)

TL;DR

This paper introduces a low-cost approximation method for well-founded justification and domination in logic programming, enhancing propagation efficiency in ASP solvers by using dominator computations in flowgraphs.

Contribution

It proposes a novel, efficient approximation technique for WFJ and WFD using dominator algorithms, extending the capabilities of ASP solvers for reachability and related problems.

Findings

Approximate WFJ and WFD can be efficiently computed using dominator algorithms.

The method simulates WFJ and WFD effects for classes of logic programs including reachability.

The approach improves propagation in ASP solving by incorporating well-founded inferences.

Abstract

Many native ASP solvers exploit unfounded sets to compute consequences of a logic program via some form of well-founded negation, but disregard its contrapositive, well-founded justification (WFJ), due to computational cost. However, we demonstrate that this can hinder propagation of many relevant conditions such as reachability. In order to perform WFJ with low computational cost, we devise a method that approximates its consequences by computing dominators in a flowgraph, a problem for which linear-time algorithms exist. Furthermore, our method allows for additional unfounded set inference, called well-founded domination (WFD). We show that the effect of WFJ and WFD can be simulated for a important classes of logic programs that include reachability. This paper is a corrected and extended version of a paper published at the 12th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2013). It has been adapted to exclude Theorem 10 and its consequences, but provides all missing proofs.