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

arXiv: https://arxiv.org/abs/1702.07461 · HTML: https://mlsanity.com/paper/1702.07461/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Feb 2017.

## Built on by (most cited first, 4 of 4)

- [Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches](https://mlsanity.com/paper/2107.08252/) (2021)
- [Aggregate Semantics for Propositional Answer Set Programs](https://mlsanity.com/paper/2109.08662/) (2021)
- [Unifying Framework for Optimizations in non-boolean Formalisms](https://mlsanity.com/paper/2206.07862/) (2022)
- [EZSMT Version 3, Matured](https://mlsanity.com/paper/2607.13344/) (2026)

## Abstract (arXiv)

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.