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.