# On Relation between Constraint Answer Set Programming and Satisfiability Modulo Theories

## TL;DR

This paper establishes a precise formal connection between constraint answer set programming and satisfiability modulo theories, enabling the use of SMT solvers for answer set computation.

## Contribution

It provides a formal translation from constraint answer set programs with linear constraints to SMT, bridging the two fields and fostering cross-disciplinary advancements.

## Key findings

- Formal relation between constraint answer set programming and SMT established
- Translation enables use of SMT solvers for answer set computation
- Facilitates cross-fertilization of theoretical and practical methods

## 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 booster 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.