Integration of Minimal Reasons in AMOSUM Constraints
TL;DR
This paper proposes and formalizes two new minimization algorithms that guarantee subset-minimal reasons and ensures cardinality-minimal reasons in the AMOSUM constraint and demonstrates that extending the solver wasp with these minimization strategies leads to substantial performance improvements.
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 .