Generalizing Level Ranking Constraints for Monotone and Convex Aggregates

TL;DR

This paper develops a generalized framework for level ranking constraints in answer set programming, enabling more systematic translation of aggregate-based extensions into various KR formalisms like SAT, SMT, and MIP.

Contribution

It introduces a uniform approach to rewrite ranking constraints that preserve aggregate structures, facilitating improved translation and solver integration for ASP extensions.

Findings

Generalized ranking constraints for monotone and convex aggregates.

Preservation of aggregate structures in translation-based ASP.

Enhanced potential for solver pipeline implementations.

Abstract

In answer set programming (ASP), answer sets capture solutions to search problems of interest and thus the efficient computation of answer sets is of utmost importance. One viable implementation strategy is provided by translation-based ASP where logic programs are translated into other KR formalisms such as Boolean satisfiability (SAT), SAT modulo theories (SMT), and mixed-integer programming (MIP). Consequently, existing solvers can be harnessed for the computation of answer sets. Many of the existing translations rely on program completion and level rankings to capture the minimality of answer sets and default negation properly. In this work, we take level ranking constraints into reconsideration, aiming at their generalizations to cover aggregate-based extensions of ASP in more systematic way. By applying a number of program transformations, ranking constraints can be rewritten in a general form that preserves the structure of monotone and convex aggregates and thus offers a uniform basis for their incorporation into translation-based ASP. The results open up new possibilities for the implementation of translators and solver pipelines in practice.