Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard

TL;DR

This paper refines the complexity bounds for ASP consistency checking by incorporating treewidth and strongly-connected components, leading to more efficient algorithms for certain classes of programs.

Contribution

It introduces a new complexity bound for ASP based on treewidth and strongly-connected components, along with a dynamic programming algorithm and a reduction to SAT.

Findings

ASP consistency is solvable in exponential time based on treewidth and component size.

The new bound improves previous results by considering strongly-connected components.

A practical dynamic programming algorithm is provided for ASP with bounded treewidth.

Abstract

It is well-know that deciding consistency for normal answer set programs (ASP) is NP-complete, thus, as hard as the satisfaction problem for classical propositional logic (SAT). The best algorithms to solve these problems take exponential time in the worst case. The exponential time hypothesis (ETH) implies that this result is tight for SAT, that is, SAT cannot be solved in subexponential time. This immediately establishes that the result is also tight for the consistency problem for ASP. However, accounting for the treewidth of the problem, the consistency problem for ASP is slightly harder than SAT: while SAT can be solved by an algorithm that runs in exponential time in the treewidth k, it was recently shown that ASP requires exponential time in k \cdot log(k). This extra cost is due checking that there are no self-supported true atoms due to positive cycles in the program. In this paper, we refine the above result and show that the consistency problem for ASP can be solved in exponential time in k \cdot log({\lambda}) where {\lambda} is the minimum between the treewidth and the size of the largest strongly-connected component in the positive dependency graph of the program. We provide a dynamic programming algorithm that solves the problem and a treewidth-aware reduction from ASP to SAT that adhere to the above limit.