Model Checker For Recursive Aggregates

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.