Technical Report: Inconsistency in Answer Set Programs and Extensions

TL;DR

This paper investigates the causes of inconsistency in Answer Set Programming and HEX-programs, introduces methods for analyzing and explaining these inconsistencies, and presents a new evaluation algorithm with significant performance improvements.

Contribution

It offers a novel framework for characterizing and explaining inconsistencies in ASP and HEX-programs, along with an innovative evaluation algorithm utilizing conflict-driven learning.

Findings

New characterization of inconsistency in ASP and HEX-programs

Techniques for computing inconsistency reasons

Significant speedup in HEX-program evaluation experiments

Abstract

Answer Set Programming (ASP) is a well-known problem solving approach based on nonmonotonic logic programs. HEX-programs extend ASP with external atoms for accessing arbitrary external information, which can introduce values that do not appear in the input program. In this work we consider inconsistent ASP- and HEX-programs, i.e., programs without answer sets. We study characterizations of inconsistency, introduce a novel notion for explaining inconsistencies in terms of input facts, analyze the complexity of reasoning tasks in context of inconsistency analysis, and present techniques for computing inconsistency reasons. This theoretical work is motivated by two concrete applications, which we also present. The first one is the new modeling technique of query answering over subprograms as a convenient alternative to the well-known saturation technique. The second application is a new evaluation algorithm for HEX-programs based on conflict-driven learning for programs with multiple components: while for certain program classes previous techniques suffer an evaluation bottleneck, the new approach shows significant, potentially exponential speedup in our experiments. Since well-known ASP extensions such as constraint ASP and DL-programs correspond to special cases of HEX, all presented results are interesting beyond the specific formalism.