# Translation-Based Constraint Answer Set Solving

Christian Drescher and **Toby Walsh**
NICTA and University of New South Wales, Sydney, Australia

## Abstract

We solve constraint satisfaction problems through translation to answer set programming (ASP).

Our reformulations have the property that unitpropagation in the ASP solver achieves well defined local consistency properties like arc, bound and range consistency. Experiments demonstrate the computational value of this approach.

## 1 Introduction

Several formalisms have been proposed for representing and solving combinatorial problems: constraint programming (CP; [Rossi *et al.*, 2006]), answer set programming
(ASP; [Baral, 2003]), propositional satisfiability checking
(SAT; [Biere *et al.*, 2009]), its extension to satisfiability modulo theories (SMT; [Nieuwenhuis *et al.*, 2006]), and many more. Each has its particular strengths: for example, CP
systems support global constraints, SAT often exploits very efficient implementations, whilst ASP systems permit recursive definitions and offer default negation. As a nonmonotonic reasoning paradigm, ASP is particularly adequate for common-sense reasoning and modelling of dynamic and incomplete knowledge, and was put forward as a powerful paradigm to solve constraint satisfaction problems (CSP) in [Niemel¨a, 1999]. Moreover, modern ASP
solvers have experienced dramatic improvements in their performance [Gebser *et al.*, 2007] and compete with the best SAT solvers. Empirical comparisons with CP have shown that, whilst ASP encodings are often highly competitive and more elaboration tolerant, non-propositional constructs like global constraints are more efficiently handled by CP systems [Dovier *et al.*, 2005].

This led to the integration of CP with ASP in *hybrid* frameworks, most notably constraint answer set programming (CASP; [Gebser *et al.*, 2009b]). Similar to SMT, the key idea of a *hybrid* approach is that theory-specific solvers interact in order to compute solutions to the whole constraint model. However, the elaboration of constraint interdependencies from different solver types is limited by the restricted interface between the ASP and the CP solver.

This paper puts forward a *translation-based* approach rather than a *hybrid* one. In this approach, all parts of the CSP model are mapped into ASP for which highly efficient solvers are available. We make several contributions to the study of translation into ASP [Drescher and Walsh, 2010]:
- We consider four different but generic encodings: the direct, support, bound and range encoding. Each represents constraints in a different way.

- We provide theoretical results on their propagation strength, i.e., what type of local consistency is achieved by the unit-propagation of an ASP solver.

- We illustrate our approach on the popular ALL-DIFFERENT constraint. This ensures that a set of variables take all different values. Unit-propagation on our encodings can simulate complex propagation algorithms with a similar overall runtime complexity.

- We conduct experiments on CSPLib [Gent and Walsh, 1999], a large problem library widely used for benchmarking by the CP community. Our results demonstrate the competitiveness of this approach.

## 2 Background

Answer Set Programming As a form of logic programming oriented towards solving CSP, ASP comes with an expressive but simple modelling language. Formally, a logic program over a set of primitive propositions A, **⊥ ∈ A**, is a finite set of *rules* r of the form h ← a1, . . . , am, not am+1**, . . . , not a**n where h, ai ∈ A are *atoms*, 1 ≤ i ≤ n. A
literal is an atom a or its default negation **not a**.

The special atom ⊥ denotes a proposition that is always false. For a rule r, define **head**(r) = h and body(r) = {a1, . . . , am, not am+1**, . . . , not a**n}. Furthermore, let **body**(r)
+ = {a1**, . . . , a**m} and **body**(r)
− =
{am+1**, . . . , a**n}. A rule r with **head**(r) = ⊥ is widely referred to as an *integrity constraint*. The semantics of a logic program is given by its answer sets, which are the key objects of interest in this paradigm. Given a logic program P over A, a set X ⊆ A is an *answer set* of P iff X is the ⊆-minimal model of the *reduct* [Gelfond and Lifschitz, 1988]
P
X = {head(r) ← **body**(r)
+ | r ∈ **P, body**(r)
− ∩ X = ∅}.

Intuitively, a rule r of the form above can be seen as a condition on the answer sets of a logic program, stating that if a1**, . . . , a**m are in the answer set and none of am+1**, . . . , a**n is