Answer Set Counting and its Applications

Abstract:

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. Importantly, a variety of probabilistic applications in reasoning or logic programming require counting answer sets. Akin to the early days of propositional model counting, state-of-the-art answer set counters do not scale well beyond small instances. While counting can be done by enumeration, simple enumeration becomes infeasible if the answer set count is high.

In this thesis, we propose efficient counting techniques for answer sets, overcoming the scalability issues faced by existing answer set systems. We propose two new ASP counting frameworks, called (i) sharpASP and (ii) sharpASP-SR. Both frameworks count answer sets avoiding larger input formulas. These techniques rely on an alternative way of defining answer sets. For sharpASP, these alternative definition allows for the lifting of key techniques developed in the context of propositional model counting to answer set counting; while for sharpASP-SR, the definition facilitates an efficient reduction of answer set counting into projected model counting.

We present a scalable approach to approximate counting for ASP. Our approach is based on systematically adding parity (xor) constraints to ASP programs, which divide the search space. We prove that adding random xor constraints partitions the answer sets of an ASP program. In practice, we use a Gaussian elimination-based x approach by lifting ideas from SAT to ASP and integrate it into a state of the art ASP solver, which we call ApproxASP. Finally, our experimental evaluation shows the scalability of our approach over existing ASP systems.

The thesis also focuses on the applications of answer set counting — we demonstrate applications in the domain of network reliability, systems biology, and minimal models. The thesis proposes a new ASP counting based framework, RelNet-ASP, to approximate the reliability of a system or network, reducing the problem of reliability estimation to an approximate answer set counting problem, offering formal guarantees of the estimated reliability. Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains; e.g., systems biology. In this thesis, we formulate several meaningful counting problems in BNs, which provide valuable insights within BN theory. We propose novel methods based on approximate counting to address these computational problems, leveraging techniques from answer set programming. Minimal models of a Boolean formula play a pivotal role in various reasoning tasks. We introduce two novel techniques for counting minimal models, leveraging the expressive power of answer set programming: the first technique employs methods from knowledge compilation, while the second one draws on recent advancements in hashing-based approximate model counting. Through empirical evaluations, we demonstrate that our proposed ASP-counting based techniques in diverse domains outperform state-of-the-art techniques in terms of both runtime performance and accuracy.