Functional Stable Model Semantics and Answer Set Programming Modulo Theories

TL;DR

This paper explores the role of functional stable model semantics in Answer Set Programming Modulo Theories, showing how tight ASPMT programs can be translated into SMT instances.

Contribution

It demonstrates the importance of functional stable model semantics in ASPMT and provides a translation method for tight ASPMT programs into SMT instances.

Findings

Functional stable model semantics is crucial in ASPMT.

Tight ASPMT programs can be translated into SMT instances.

Existing ASP integration approaches are special cases with limited functions.

Abstract

Recently there has been an increasing interest in incorporating ``intensional'' functions in answer set programming. Intensional functions are those whose values can be described by other functions and predicates, rather than being pre-defined as in the standard answer set programming. We demonstrate that the functional stable model semantics plays an important role in the framework of ``Answer Set Programming Modulo Theories (ASPMT)'' -- a tight integration of answer set programming and satisfiability modulo theories, under which existing integration approaches can be viewed as special cases where the role of functions is limited. We show that ``tight'' ASPMT programs can be translated into SMT instances, which is similar to the known relationship between ASP and SAT.