Eliminating Unfounded Set Checking for HEX-Programs

TL;DR

This paper introduces a syntactic class of HEX-programs that can be evaluated more efficiently by skipping unfounded set checks, significantly improving HEX-program solving performance.

Contribution

It identifies a new syntactic class of HEX-programs enabling complete avoidance of unfounded set checks, and proposes decomposition criteria to further optimize evaluation.

Findings

Efficient recognition of the syntactic class reduces computational overhead.

Decomposition criteria allow targeted unfounded set checks.

Preliminary experiments indicate improved evaluation efficiency.

Abstract

HEX-programs are an extension of the Answer Set Programming (ASP) paradigm incorporating external means of computation into the declarative programming language through so-called external atoms. Their semantics is defined in terms of minimal models of the Faber-Leone-Pfeifer (FLP) reduct. Developing native solvers for HEX-programs based on an appropriate notion of unfounded sets has been subject to recent research for reasons of efficiency. Although this has lead to an improvement over naive minimality checking using the FLP reduct, testing for foundedness remains a computationally expensive task. In this work we improve on HEX-program evaluation in this respect by identifying a syntactic class of programs, that can be efficiently recognized and allows to entirely skip the foundedness check. Moreover, we develop criteria for decomposing a program into components, such that the search for unfounded sets can be restricted. Observing that our results apply to many HEX-program applications provides analytic evidence for the significance and effectiveness of our approach, which is complemented by a brief discussion of preliminary experimental validation.