Answer set programming (ASP) is a popular declarative programming paradigm with various applications. Programs can easily have many answer sets that cannot be enumerated in practice, but counting still allows quantifying solution spaces. If one counts under assumptions on literals, one obtains a tool to comprehend parts of the solution space, so-called answer set navigation. However, navigating through parts of the solution space requires counting many times, which is expensive in theory. Knowledge compilation compiles instances into representations on which counting works in polynomial time. However, these techniques exist only for CNF formulas, and compiling ASP programs into CNF formulas can introduce an exponential overhead. This paper introduces a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. Our anytime technique uses the inclusion-exclusion principle to improve bounds by over- and undercounting systematically. In a preliminary empirical analysis, we demonstrate promising results. After compiling the input (offline phase), our approach quickly (re)counts.

翻译：回答集编程是一种流行的声明式编程范式，具有广泛的应用。程序可能包含大量无法在实践中枚举的回答集，但计数仍能量化解空间。若在文字假设下进行计数，则可获得理解解空间各部分的工具，即所谓的回答集导航。然而，遍历解空间各部分的计数需要多次执行，这在理论上代价高昂。知识编译将实例转化为可在多项式时间内完成计数的表示形式，但这些技术仅适用于CNF公式，且将回答集程序编译为CNF公式可能引入指数级开销。本文提出一种技术，通过在编码支持模型的知识编译CNF上迭代式回答集计数。我们的即时技术利用容斥原理，通过系统性过计数与欠计数来优化边界。初步实证分析展示了令人鼓舞的结果：在完成输入编译（离线阶段）后，该方法能快速完成（重新）计数。