Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?

TL;DR

This paper introduces a treewidth-aware reduction from normal ASP to SAT, showing that normal ASP is slightly harder than SAT in terms of treewidth, and demonstrates improved practical performance with heuristics.

Contribution

The paper presents the first treewidth-preserving reduction from normal ASP to SAT and establishes the inherent complexity difference between them.

Findings

The reduction guarantees only a slight increase in treewidth.

Normal ASP is proven to be slightly harder than SAT regarding treewidth.

Empirical results show the new reduction outperforms existing translations with heuristics.

Abstract

Answer Set Programming (ASP) is a paradigm for modeling and solving problems for knowledge representation and reasoning. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A generic parameter in parameterized complexity originating from graph theory is the so-called treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there are translations from (normal) ASP to SAT, no reduction that preserves treewidth or at least keeps track of the treewidth increase is known. In this paper we propose a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Further, we show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable. Finally, we present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decomposition heuristics. Overall, our reduction works better with these heuristics than existing translations.