Model checking for disjunctive logic programs is a co-NP-complete task for which two main state-of-the-art approaches exist: one based on the unsatisfiability of SAT formulas derived from program reducts, and another based on unfounded sets. Although both are effective and efficient, their original formulations do not support recursive aggregates. This paper extends previous work by tackling the stability check problem in the presence of such aggregates. We generalize the reduct-based approach to operate over pseudo-Boolean theories rather than SAT encodings, yielding more compact and efficient formulations. In parallel, we extend the unfounded-set-based approach to incorporate aggregates, integrating both strategies as propagators within the ASP solver clingo. Additionally, we introduce partial stability checks to enable incremental or approximate verification of model stability. Our empirical evaluation demonstrates that these novel strategies not only preserve correctness but also substantially improve the efficiency of model checking for disjunctive programs with aggregates.

Answer Set Programming (ASP) is a well-known logic-based formalism that has been used to model and solve a variety of AI problems. For several years, ASP implementations primarily focused on the main computational task: the computation of one answer set of a (logic) program. Nonetheless, several AI problems, that can be conveniently modelled in ASP, require to enumerate solutions characterized by an optimality property that can be expressed in terms of subset-minimality with respect to some objective atoms. In this context, solutions are often either (i) answer sets that are subset-minimal w.r.t. the objective atoms or (ii) atoms that are contained in all subset-minimal answer sets, or (iii) sets of atoms that enforce the absence of answer sets on the ASP program at hand — such sets are referred to as minimal unsatisfiable subsets (MUSes). In all the above-mentioned cases, the corresponding computational task is currently not supported by plain state-of-the-art ASP solvers. In this paper, we study formally these tasks and fill the gap in current implementations by proposing several algorithms to enumerate MUSes and subset-minimal answer sets, as well as perform cautious reasoning on subset-minimal answer sets. We implement our algorithms on top of wasp and perform an experimental analysis on several hard benchmarks showing the good performance of our implementation.