# Constraint Answer Set Solver EZCSP and Why Integration Schemas Matter

## TL;DR

This paper presents the first comprehensive account of the EZCSP constraint answer set solver, introduces an extension of transition systems for its algorithm, and emphasizes the importance of integration schemas in hybrid reasoning systems.

## Contribution

It provides a detailed description of EZCSP, extends transition systems for SAT solvers, and analyzes the impact of different integration schemas in hybrid answer set programming.

## Key findings

- EZCSP is a successful hybrid solver used in various applications.
- The extended transition system accurately models EZCSP's algorithm.
- Different integration schemas significantly affect the performance and design of hybrid solvers.

## Abstract

Researchers in answer set programming and constraint programming have spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming. Constraint answer set programming languages and systems proved to be successful at providing declarative, yet efficient solutions to problems involving hybrid reasoning tasks. One of the main contributions of this paper is the first comprehensive account of the constraint answer set language and solver EZCSP, a mainstream representative of this research area that has been used in various successful applications. We also develop an extension of the transition systems proposed by Nieuwenhuis et al. in 2006 to capture Boolean satisfiability solvers. We use this extension to describe the EZCSP algorithm and prove formal claims about it. The design and algorithmic details behind EZCSP clearly demonstrate that the development of the hybrid systems of this kind is challenging. Many questions arise when one faces various design choices in an attempt to maximize system's benefits. One of the key decisions that a developer of a hybrid solver makes is settling on a particular integration schema within its implementation. Thus, another important contribution of this paper is a thorough case study based on EZCSP, focused on the various integration schemas that it provides. Under consideration in Theory and Practice of Logic Programming (TPLP).