Translation-Based Constraint Answer Set Solving

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 non-monotonic reasoning paradigm, ASP is particularly adequate for commonsense 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 ALLDIFFERENT 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

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 an}. Furthermore, let body(r)+ = {a1, . . . , am} and body(r)- = {am+1, . . . , an}. 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]

= {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, . . . , am are in the answer set and none of am+1, . . . , an is included, then h must be in the set. We also consider extensions to logic programs, such as choice rules and cardinality rules. A choice rule of the form

{h1, . . . , hk} ← a1, . . . , am, not am+1, . . . , not an allows for the nondeterministic choice over atoms in {h1, . . . , hk}. A cardinality rule of the form

infers h if k or more literals in the set {a1, . . . , am, not am+1, . . . , not an} are satisfied. The semantics of choice rules and cardinality rules is given through program transformations (cf. [Simons et al., 2002]). Note that aggregations and other forms of set constructions are also common in ASP. However, we will limit ourselves to the above concepts as they are expressive enough for what follows. Also note that, although answer set semantics is propositional, atoms in A can be constructed from a first-order signature. The logic program over A is then obtained by a grounding process, systematically substituting all occurrences of first-order variables with terms formed by function symbols and constants given through the signature. The task of ASP systems is to compute answer sets for logic programs. A successful framework is conflict-driven nogood learning (CDNL;[Gebser et al., 2007]). It reflects conditions from program rules in a set of nogoods, and describes ASP inference as unit-propagation on nogoods to determine logical consequences.

Constraint Satisfaction and Consistency We want to use ASP to model and solve CSP. Formally, a CSP is a triple (V,D,C) where V is a finite set of variables, each v ∈ V has an associated finite domain dom(v) ∈ D, and C is a set of constraints. A constraint c is a pair (RS, S) where RS is a k-ary relation, denoted range(c), on the variables in S ∈ V k , denoted scope(c). Given a (constraint variable) assignment A : V → ⋃v∈V dom(v), for a constraint c with scope(c) = S = (v1, . . . , vk) define A(S) = (A(v1), . . . ,A(vk)) and call c satisfied if A(S) ∈ range(c). Define the set of constraints satisfied by A as satC(A) = {c | A(scope(c)) ∈ range(c), c ∈ C}. A binary constraint c has |scope(c)| = 2. For instance, the constraint v1 ̸= v2 ensures that v1 and v2 take different values. An n-ary constraint c has parametrised scope. For instance, ALL-DIFFERENT ensures that a set of variables, |scope(c)| = n, take all different values. As any non-binary constraint, this can be decomposed into binary constraints, i.e., O(n2 ) constraints vi ̸= vj for i < j. However, as we shall see in the following, such reformulation can hinder inference.

An assignment A is a solution to a CSP iff it satisfies all constraints in C. Typically, CP systems use backtracking search to explore assignments in a search tree. In a search tree, each node represents an assignment to some variables, child nodes are obtained by selecting an unassigned variable and having a child node for each possible value for this variable, and the root node is empty. Every time a variable is assigned a value, constraint propagation is executed, pruning the set of values for the other variables, i.e., enforcing a certain type of local consistency such as arc, bound, range, or domain consistency. A binary constraint c is arc consistent iff a variable v1 ∈ scope(c) is assigned any value d1 ∈ dom(v1), there exists a compatible value d2 ∈ dom(v2)

for the other variable v2. An n-ary constraint c is domain consistent iff a variable vi ∈ scope(c) = {v1, . . . , vn} is assigned any value di ∈ dom(vi), there exist compatible values in the domains of all the other variables dj ∈ dom(vj), 1 ≤ j ≤ n, j ̸= i. Bound and range consistency are defined for constraints over finite intervals. A constraint c is bound consistent iff a variable vi is assigned di ∈ {min(dom(vi)),max(dom(vi))} there exist consistent values between the minimum and maximum domain value for all the other variables in the scope of the constraint, called a bound support. A constraint is range consistent iff a variable is assigned any value in its domain, there exists a bound support. Range consistency is in between domain and bound consistency, where domain consistency is the strongest of the three local consistency properties.

Constraint Answer Set Programming Constraint logic programming naturally merges CP and logic programming, while preserving the advantages of either approach to modelling and solving CSP. Formally, a constraint logic program is a logic program P over an alphabet distinguishing regular atoms A and constraint atoms C, such that head(r) ∈ A for each r ∈ P [Gebser et al., 2009b]. A function γ : C → C associates constraint atoms with constraints. (The set C stems from the definition of CSP.) For sets of constraints C′ ⊆ C define γ(C ′ ) = {γ(c) | c ∈ C ′ }. Given a constraint logic program P over A and C, and an assignment A, a set X ⊆ A is a constraint answer set of P with respect to A iff X is an answer set of the constraint reduct [Gebser et al., 2009b]:

The idea in our translation-based approach to constraint answer set solving is to compile a constraint logic program into a (normal) logic program by adding an ASP reformulation of constraint variables and all constraints that appear in the constraint logic program. This allows us to apply CDNL to compute constraint answer sets. A key advantage is that nogood learning techniques can exploit constraint interdependencies since all variables will be shared between constraints. This can improve propagation between constraints. Our reformulations also provides a propagator for the negation of a constraint.

3 Reformulating CASP into ASP

We now present four ASP encodings for variables and constraints over finite domains. All constraints c are reified via atoms sat(c), and violate(c), indicating whether c is satisfied or violated, respectively. To ensure consistency, i.e., either sat(c) or violate(c) is in an answer set, we post

for every constraint c. Other representations, e.g., using choice rules, are also possible. To save the reader frommultiple superscripts, in the following, we will assume dom(v) = [1, d] for all v ∈ V .

Direct Encoding A straightforward encoding is the direct encoding in which an atom e(v, i) is introduced for each constraint variable v and each value i from their domain, representing v = i. Intuitively, e(v, i) is in an answer set if v takes the value i, and it is not if v takes a value different from i. For each v, possible assignments are encoded by a choice rule (1). Furthermore, we specify that v takes at least one value (2) and that it takes at most one value (3).

A constraint c is encoded as forbidden combination of values, i.e., if v1 = d1, v2 = d2, . . . , vn = dn is such a forbidden combination then we encode

Unfortunately, the direct encoding hinders propagation:

Theorem 1 Enforcing arc consistency on the binary decomposition of a constraint prunes more values from the variables domain than unit-propagation on its direct encoding.

The support encoding has been proposed in the domain of SAT to tackle this weakness [Gent, 2002].

Support Encoding We now encode support information for assignments rather than the encoding of conflicts. For each possible assignment to a variable one of its supports must hold, that is, the set of values for the other variable which allow this assignment. Formally, a support for a constraint variable v to take the value i across a constraint c is the set of values {i1, . . . , im} ⊆ dom(v′ ) of another variable in v′ ∈ scope(c)\{v} which allow v = i, and can be encoded in the following rule, based on (1-3):

It can be read as whenever v = i, then at least one of its supports must hold, otherwise the constraint is violated. In the support encoding, for each constraint c there is one support for each pair of distinct variables v, v′ ∈ scope(c), and for each value i.

Theorem 2 Unit-propagation on the support encoding enforces arc consistency on the binary decomposition of the original constraint.

We have used program transformation [Simons et al., 2002] in [Drescher and Walsh, 2010] to reformulate ALLDIFFERENT straightforwardly according to our support encoding into O(d) cardinality rules:

Corollary 1 Unit-propagation on (1-4) enforces arc consistency on the binary decomposition of ALL-DIFFERENT in O(nd2 ) down any branch of the search tree.

Range Encoding In the range encoding, we represent that a variable can take values from an interval v ∈ [l, u], i.e., a value between l and u (inclusive). An atom r(v, l, u) is introduced for each v and [l, u] ⊆ [1, d]. For each range [l, u], the following O(nd2 ) rules encode v ∈ [l, u] whenever v ̸∈

[1, l - 1] and v ̸∈ [u + 1, d], and enforce a consistent set of ranges, i.e., v ∈ [l, u] implies v ∈ [l-1, u] and v ∈ [l, u+1]:

Constraints are encoded into integrity constraints representing conflict regions v1 ∈ [l1, u1], . . . , vn ∈ [ln, un]:

Theorem 3 Unit-propagation on the range encoding enforces range consistency on the original constraint.

An efficient propagator for ALL-DIFFERENT enforces range consistency by pruning Hall intervals [Leconte, 1996]. A Hall interval of size k completely contains the domains of k variables, formally, |{v | dom(v) ⊆ [l, u]}| = u-l+1. Observe that in any bound support, the variables whose domains are contained in the Hall interval consume all values within the Hall interval, whilst any other variable must find their support outside the Hall interval (cf. [Bessi`ere et al., 2009a]). We encode ALL-DIFFERENT such that no interval [l, u] can contain more variables than its size:

This simple reformulation can simulate a complex propagation algorithm like the one in [Leconte, 1996] with a similar overall complexity.

Corollary 2 Unit-propagation on (5-8) enforces range consistency on ALL-DIFFERENT in O(nd3 ) down any branch of the search tree.

Bound Encoding In our bound encoding, similar to the order encoding [Tamura et al., 2006], an atom b(v, i) is introduced for each variable v and value i to represent that v is bounded by i, i.e., v ≤ i. For each v, possible assignments are encoded by a choice rule (9). To ensure a consistent set of bounds, (10) encodes that v ≤ i implies v ≤ i + 1. Finally, (11) encodes v ≤ d, i.e., some value must be assigned to v.

Similar to the range encoding, we represent conflict regions l1 < v1 ≤ u1, . . . , ln < vn ≤ un as below

Theorem 4 Unit-propagation on the bound encoding enforces bound consistency on the original constraint.

In order to achieve a reformulation of ALL-DIFFERENT that can only prune bounds, the bound encoding for variables is linked to (8) as follows:

Corollary 3 Unit-propagation on (8-14) enforces bound consistency on ALL-DIFFERENT in O(nd2 ) down any branch of the search tree.

4 Experiments

We have conducted experiments on hard combinatorial problems modelled with ALL-DIFFERENT constraints that stem from CSPLib [Gent and Walsh, 1999]. Experiments consider different options in our translation-based approach to constraint answer set solving. We denote the support encoding by S, the bound encoding by B, and the range encoding by R. To explore the impact of small Hall intervals, we also tried Bk and Rk, an encoding with only those cardinality rules (8) for which u - l + 1 ≤ k. The consistency achieved by Bk and Rk may be weaker than bound and range consistency, respectively, when k < n. We also include the hybrid CASP systems clingcon (0.1.2), and ezcsp (1.6.9) in our empirical analysis. While clingcon extends the ASP system clingo (2.0.2) with the CP solver gecode (2.2.0), ezcsp combines the grounder gringo (2.0.3) and ASP solver clasp (1.3.0) with sicstus (4.0.8) as CP solver. (Note that the system clingo combines the grounder gringo and ASP solver clasp in a monolithic way.) To provide a representative comparison with clingcon and ezcsp, we have applied clingo (2.0.3) to the encodings in our translation-based approach. To compare the performance of constraint answer set solvers against traditional CP, we also report results of gecode (3.2.0). Its heuristic for variable selection was set to a smallest domain as in clingcon. All experiments were run on a 2.00 GHz PC under Linux. We report results in seconds, where each run was limited to 600 s time and 1 GB RAM.

PigeonHole Problems The famous pigeon hole problem is to show that it is not possible to assign n pigeons to n-1 holes if each pigeon must be assigned a distinct hole. As can be seen from the results shown in Table 1, our bound and range encodings perform significantly faster compared to weaker encodings and the other options using filtering algorithms for the ALL-DIFFERENT constraint that achieve arc consistency on its binary decomposition. However, as can be expected on such problems, detecting large Hall intervals is essential.

Quasigroup Completion A quasigroup is an algebraic structure over n elements and can be represented by an n×nmultiplication table such that each element in the structure occurs exactly once in each row and each column of the table. The quasigroup completion problem is to show whether a partially filled table can be completed to a multiplication table of a quasigroup. We have included models for gecode that enforce bound and domain consistency on ALL-DIFFERENT, denoted gecodeB and gecodeD, respectively, in our experiments. Table 2 gives the runtime for solving QCP of size n = 20. The left-most column gives the ratio of preassigned entries. The results demonstrate phase transition behaviour in the systems ezcsp, clingcon, gecode, and gecodeB, while our ASP encodings and gecodeD (not shown) solve all problems within seconds. We conclude that learning constraint interdependencies as in our approach (using CDNL) is sufficient to tackle quasigroup completion, i.e., specialised algorithms that enforce domain consistency are not necessary.

Quasigroup Existence The quasigroup existence problem is to determine the existence of certain interesting classes of quasigroups with some additional properties ([Fujita et al., 1993]). The properties are represented by axioms #1 - #7 in the direct encoding. In ezcsp and gecode, we additionally use constructive disjunction. Their logic programming equivalent are integrity constraints, exploited in the options S, Bk, Rk and clingcon. As for ezcsp and clingcon on benchmark classes #1 to #4, our resuls presented in Table 3 suggest that both constructive disjunction and integrity constraints have a similar behaviour. However, our encodings benefit again from learning constraint interdependencies, resulting in runtimes that outperform all other systems including gecode on the hardest problems.

Graceful Graphs A labelling of the nodes in a graph (V,E) is graceful if it assigns a unique label from the integers in [0, |E|] such that, when each edge is labelled with the distance between its nodes' labels, the resulting edge labels are all different. The graceful graph problem is to determine the existence of such a labelling. We use auxiliary variables for edge labels. Their relation to node labels is represented in the direct encoding which weakens the overall consistency. Table 4 shows our results for double wheel graphs, i.e., graphs composed of two copies of a cycle with n nodes, each connected to a central hub. Our encodings compete with ezcsp and outperform the other systems, whilst the support encoding performs better than bound and range encodings. We observe some variability in the results for Bk and Rk, e.g., for n = 8 the options B1 and B solve the problem within the time limit but B3 does not, although B3 contains B1. We explain this variability by the lookback-based branching heuristic used by clingo being misled by the extra variables introduced in Bk and Rk. This is inherent to a growing size of the encoding.

5 RelatedWork

Most previous work integrates CP techniques into ASP to avoid huge ground instantiations given through logic programs with first-order variables over large domains. An ASP system was extended in [Baselice et al., 2005; Mellarkod and Gelfond, 2008; Mellarkod et al., 2008] such that it does not require full grounding, since variables and limitations on their domains can be handled in the CP solver. A similar approach presented in [Dal Pal`u et al., 2009] employs the CP solver to compute also the answer sets. Although these hybrid strategies potentially eliminate the bottleneck that is inherent to the translation-based approach, they view ASP and CP solvers as blackboxes which do not match the performance of state-of-the-art SMT solvers. In particular, they do not make use of conflict-driven learning and back-jumping techniques. This gap was closed by the approach taken in [Gebser et al., 2009b] following the one by SMT solvers in letting the ASP solver deal with the propositional structure of the logic program, while a CP solver addresses the constraints. Apart from extending the unit-propagation of an ASP solver through constraint propagation, it deals with the elaboration of reasons for atoms derived by constraint propagation within conflict resolution. The elaboration of conflict information from constraint propagators, however, is limited since constraint propagators lack support for this feature (they would have to keep an implication graph to record reasons for each propagation step). Hence, the conflict resolution process cannot exploit constraint interdependencies. A different hybrid approach to solving CASP is presented in [Balduccini, 2009], where an answer set of a logic program with constraint atoms encodes a desired CSP which, in turn, is handled by a CP system. A more general framework using multiple declarative paradigms to specify CSP is proposed in [J¨arvisalo et al., 2009]. Either approach, however, restricts communication between different solver types in order to compute solutions to the whole CASP model, e.g., they also do not incorporate conflict-driven learning and back-jumping techniques.

In a translation-based approach, all parts of the model are mapped into a single constraint language for which highly efficient off-the-shelf solvers are available. Hence, related work has mostly focussed on the translation of constraints to SAT (cf. [Walsh, 2000; Gent, 2002]). Translation into ASP, however, can be more general than translation into SAT: Every nogood can be syntactically represented by a clause, but other ASP constructs are also possible, such as cardinality and weight constraints [Simons et al., 2002]. ASP was put forward as a novel paradigm for modelling and solving CSP in [Niemel¨a, 1999], where straightforward encodings to represent generic constraints via either allowed or forbidden combination of values has been presented. Preliminary work on translating CASP into ASP was conducted in [Gebser et al., 2009a], but they did not consider what level of consistency was achieved by their translation.

Decompositions of ALL-DIFFERENT into simple arithmetic constraints such that bound and range consistency can be achieved were proposed in [Bessi`ere et al., 2009a]. There is no polynomial-sized decomposition that achieves domain consistency [Bessi`ere et al., 2009b].

6 Conclusions

We have shown that constraint answer set programming is a promising approach to representing and solving combinatorial problems that naturally merges CP and ASP, while preserving the advantages of both paradigms. We have presented a translation-based approach to constraint answer set solving. In particular, we have proposed various generic ASP encodings for constraints on finite domains such that the unitpropagation of an ASP solver achieves a certain type of local consistency. We have formulated our techniques as a preprocessor that can be applied to existing ASP systems without changing their source code. This allows for programmers to select the solver that best fit their needs. An empirical evaluation of the computational impact on benchmarks from CP has shown our approach outperforming CP and hybrid CASP systems on most instances. As a key advantage we have identified that CDNL exploits constraint interdependencies which can improve propagation between constraints.

Future work concerns the combination of our translationbased approach with a hybrid CASP system centred around lazy nogood generation (cf. lazy clause generation in [Ohrimenko et al., 2009]) to combine the advantages of either approach. We will also explore the different choices that arise from this combination.

Acknowledgements NICTA is funded by the Department of Broadband, Communications and the Digital Economy, and the Australian Research Council.