Integration of Minimal Reasons in AMOSUM Constraints

Full abstract

Read the full abstract

Answer Set Programming (ASP) is a robust paradigm for knowledge representation and reasoning, yet the efficient management of complex, overlapping constraints remains a critical challenge for modern solvers. Among the constructs proposed to address this issue, the AMOSUM constraint provides a unified abstraction that integrates SUM and At-Most-One (AMO) properties within a single propagator. In this paper, we extend AMOSUM by introducing novel reason minimization techniques aimed at improving propagation quality and enhancing search space pruning. While the original propagator performs standard literal propagation, we propose and formalize two new minimization algorithms: min , which guarantees subset-minimal reasons, and cmin , which ensures cardinality-minimal reasons. In addition, we provide formal proofs of correctness and complexity for both algorithms and show that computing a cardinality-minimal reason is an F Δ 2 P -complete problem. An extensive empirical evaluation on diverse benchmark suites demonstrates that extending the solver wasp with these minimization strategies leads to substantial performance improvements. Moreover, our enhanced system, amowasp , consistently outperforms the minimization-free configuration, and is competitive with the state-of-the-art solver clingo .