Answer Set Counting and its Applications

TL;DR

This paper addresses exact and approximate counting of answer sets in ASP, formalizing the problems $|\,\mathsf{AS}(P)\,|$ and its probabilistic counterpart. It introduces SharpASP, an exact counter that employs a two-formula framework with $F=\mathsf{Comp}(P)$ and $G=\mathsf{Copy}(P)$ to prune search space, and ApproxASP, an approximate counter using XOR-based hashing with Gauss–Jordan elimination to deliver $(\varepsilon,\delta)$ guarantees. Empirical results on a large benchmark suite show SharpASP significantly outperforms prior exact counters, while ApproxASP performs well on disjunctive programs and remains competitive with ApproxMC on normal programs, illustrating practical scalability. The work demonstrates applicability to real-world problems (e.g., network reliability) and outlines future directions, including extending SharpASP to disjunctive programs and integrating strengths from other counters to broaden applicability.

Abstract

We have focused on Answer Set Programming (ASP), more specifically, answer set counting, exploring both exact and approximate methodologies. We developed an exact ASP counter, sharpASP, which utilizes a compact encoding for propositional formulas, significantly enhancing efficiency compared to existing methods that often struggle with inefficient encodings. Our evaluations indicate that sharpASP outperforms current ASP counters on several benchmarks. In addition, we proposed an approximate ASP counter, named ApproxASP, a hashing-based counter integrating Gauss-Jordan elimination within the ASP solver, clingo. As a practical application, we employed ApproxASP for network reliability estimation, demonstrating superior performance over both traditional reliability estimators and #SAT-based methods.