On relation between constraint answer set programming and satisfiability modulo theories*. Issue 4 (28th June 2017)

• Record Type: Journal Article
• Authors: LIERLER, YULIYA; SUSMAN, BENJAMIN
• Is Part Of: Theory and practice of logic programming. Volume 17:Issue 4(2017)
• Page Start: 559
• Page End: 590
• Publication Date: 2017-06-28
• Subjects: constraint answer set programming, -- constraint satisfaction processing, -- satisfiability modulo theories; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068417000114
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. It is often informally related to the field of satisfiability modulo theories. Yet, the exact formal link is obscured as the terminology and concepts used in these two research areas differ. In this paper, we connect these two research areas by uncovering the precise formal relation between them. We believe that this work will boost the cross-fertilization of the theoretical foundations and the existing solving methods in both areas. As a step in this direction, we provide a translation from constraint answer set programs with integer linear constraints to satisfiability modulo linear integer arithmetic that paves the way to utilizing modern satisfiability modulo theories solvers for computing answer sets of constraint answer set programs.