A Uniform Treatment of Aggregates and Constraints in Hybrid ASP
This work addresses a foundational problem in hybrid ASP solving for researchers and practitioners in logic programming and AI, though it appears incremental as it builds on existing lazy SMT solving approaches.
The paper tackles the difficulty of characterizing hybrid Answer Set Programming (ASP) solving by proposing an abstract approach to treat theory terms, which enables the development of a semantic framework for hybrid ASP solving and aggregate functions for theory variables. The result shows that this framework generalizes existing aggregate semantics in ASP and can be implemented using off-the-shelf hybrid solvers.
Characterizing hybrid ASP solving in a generic way is difficult since one needs to abstract from specific theories. Inspired by lazy SMT solving, this is usually addressed by treating theory atoms as opaque. Unlike this, we propose a slightly more transparent approach that includes an abstract notion of a term. Rather than imposing a syntax on terms, we keep them abstract by stipulating only some basic properties. With this, we further develop a semantic framework for hybrid ASP solving and provide aggregate functions for theory variables that adhere to different semantic principles, show that they generalize existing aggregate semantics in ASP and how we can rely on off-the-shelf hybrid solvers for implementation.