Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches

TL;DR

This paper reviews constraint answer set programming (CASP), highlighting its hybrid nature, solver architectures, and applications, while comparing integrational and translational approaches and illustrating with a Traveling Salesman problem example.

Contribution

It provides a comprehensive overview of CASP solver designs, distinguishing between integrational and translational methods, and discusses future development directions.

Findings

CASP demonstrates promising solver development and applications.

Different approaches (integrational vs translational) have distinct design features.

CASP is positioned among other automated reasoning techniques.

Abstract

Constraint answer set programming or CASP, for short, is a hybrid approach in automated reasoning putting together the advances of distinct research areas such as answer set programming, constraint processing, and satisfiability modulo theories. Constraint answer set programming demonstrates promising results, including the development of a multitude of solvers: acsolver, clingcon, ezcsp, idp, inca, dingo, mingo, aspmt, clingo[l,dl], and ezsmt. It opens new horizons for declarative programming applications such as solving complex train scheduling problems. Systems designed to find solutions to constraint answer set programs can be grouped according to their construction into, what we call, integrational or translational approaches. The focus of this paper is an overview of the key ingredients of the design of constraint answer set solvers drawing distinctions and parallels between integrational and translational approaches. The paper also provides a glimpse at the kind of programs its users develop by utilizing a CASP encoding of Travelling Salesman problem for illustration. In addition, we place the CASP technology on the map among its automated reasoning peers as well as discuss future possibilities for the development of CASP.