Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from diverse domains in a natural way. Building on advances in propositional SAT solving, the past two decades have witnessed the emergence of well-engineered systems for solving the answer set satisfiability problem, i.e., finding models or answer sets for a given answer set program. In recent years, there has been growing interest in problems beyond satisfiability, such as model counting, in the context of ASP. Akin to the early days of propositional model counting, state-of-the-art exact answer set counters do not scale well beyond small instances. Exact ASP counters struggle with handling larger input formulas. The primary contribution of this paper is a new ASP counting framework, called sharpASP, which counts answer sets avoiding larger input formulas. This relies on an alternative way of defining answer sets that allows for the lifting of key techniques developed in the context of propositional model counting. Our extensive empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters. Specifically, by using sharpASP, we were able to solve 1062 benchmarks with PAR2 score of 3082 whereas using prior state-of-the-art, we could only solve 895 benchmarks with a PAR2 score of 4205, all other experimental conditions being the same.

翻译：答案集编程（ASP）因其能够以自然方式建模来自不同领域的困难组合问题，已成为知识表示和自动推理领域的一种有前景的范式。借助命题SAT求解的进展，过去二十年见证了用于求解答案集可满足性问题（即为给定答案集程序寻找模型或答案集）的工程化系统的涌现。近年来，在ASP背景下，人们对超越可满足性的问题（如模型计数）的兴趣日益增长。与命题模型计数的早期类似，最先进的精确答案集计数器在应对小规模实例之外的情况时扩展性不佳。精确ASP计数器在处理更大规模的输入公式方面存在困难。本文的主要贡献是提出一种名为sharpASP的新型ASP计数框架，该框架通过避免使用大规模输入公式来计算答案集。这依赖于一种替代性的答案集定义方式，使得可以借鉴命题模型计数领域开发的关键技术。我们在1470个基准测试上的广泛实证分析表明，与当前最先进的精确答案集计数器相比，该框架实现了显著的性能提升。具体而言，在相同的实验条件下，使用sharpASP我们能够解决1062个基准测试，PAR2得分为3082；而使用先前的最先进技术，我们仅能解决895个基准测试，PAR2得分为4205。