The Impact of Structure in Answer Set Counting: Fighting Cycles and Its Limits

Answer Set Programming is a widely used paradigm in knowledge representation and reasoning, which strongly relates to the satisfiability (SAT) of propositional formulas. While in the area of SAT, the last couple of years brought significant advances and different techniques for solving hard counting-based problems (e.g., #SAT, weighted counting, projected counting) that require more effort than deciding satisfiability, ASP still falls short. Intuitively, one explanation for this lies in the structure of a program, that - compared to SAT - was shown to yield strong evidence for being slightly less useful during solving. Indeed, for the structural measure treewidth that plays an important role in #SAT, ASP is expected to be at least slightly harder than SAT. The underlying source of this hardness increase lies in cyclic dependencies in the positive dependency graph. In this work, we consider which strategies are appropriate to tackle counting-based problems for ASP depending on cycle lengths. We present different encodings to counting-based variants of SAT that utilize recent advances. For small cycle lengths, we demonstrate a novel strategy based on feedback vertex sets. While medium cycle lengths leave room for future improvements, surprisingly, if cycles are significantly larger than structural dependencies (treewidth), we obtain a polynomial algorithm.