Abstract
In this talk we consider the problem of integrating answer set programming (ASP) and satisfiability modulo theories (SMT). We discuss a characterization of stable models of logic programs based on Clark’s completion and simple difference constraints. The characterization leads to a method of translating a ground logic program to a linear size theory in difference logic, i.e. propositional logic extended with difference constraints between two integer variables, such that stable models of the program correspond to satisfying assignments of the resulting theory in difference logic. Many of the state-of-the-art SMT solvers support directly difference logic. This opens up interesting possibilities. On one hand, any solver supporting difference logic can be used immediately without modifications as an ASP solver for computing stable models of a logic program by translating the program to a theory in difference logic. On the other hand, SMT solvers typically support also other extensions of propositional logic such as linear real and integer arithmetic, fixed-size bit vectors, arrays, and uninterpreted functions. This suggests interesting opportunities to extend ASP languages with such constraints and to provide effective solver support for the extensions. Using the translation an extended language including logic program rules and, for example, linear real arithmetic can be translated to an extension of propositional logic supported by current SMT solvers. We discuss the effectiveness of state-of-the-art SMT solvers as ASP solvers and the possibilities of developing extended ASP languages based on SMT solver technology.
This work is financially supported by Academy of Finland under the project Methods for Constructing and Solving Large Constraint Models (grant #122399).
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niemelä, I. (2009). Integrating Answer Set Programming and Satisfiability Modulo Theories. In: Erdem, E., Lin, F., Schaub, T. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2009. Lecture Notes in Computer Science(), vol 5753. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04238-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-04238-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04237-9
Online ISBN: 978-3-642-04238-6
eBook Packages: Computer ScienceComputer Science (R0)