Exploiting Short Supports for Generalised Arc Consistency for Arbitrary Constraints

1 Introduction

Constraint solving of a given problem proceeds in two phases. First, the problem is modelled as a set of decision variables and a set of constraints on those variables that a solution must satisfy. A decision variable represents a choice that must be made in order to solve the problem, and its associated domain of potential values corresponds to the options for that choice. In the second phase, a constraint solver searches for a solution or solutions automatically. Typically, constraint solvers employ a systematic backtracking search, interleaving the choice of an instantiation of a decision variable with the propagation of the constraints to determine the consequences of the choice made. In order to facilitate this process, each constraint supported by the solver has an associated propagation algorithm.

Propagation algorithms can broadly be divided into two types. The first are specialised to reason very efficiently about constraint patterns that occur very frequently in models. Examples include the global cardinality constraint [R´egin, 1996] and the element constraint [Gent et al., 2006b]. It is not feasible to support every possible constraint expression with a specialised propagator in this way, in which case general-purpose constraint propagators, such as GAC-Schema [Bessi`ere and R´egin, 1997] or GAC2001 [Bessi`ere et al., 2005], are used. These are typically more expensive than specialised propagators but are an important tool when no specialised propagator is available.

A support for a domain value of a variable is an explanation as to why that value cannot yet be removed from consideration in the search for a solution. It is usually given in terms of a set of literals: variable-value pairs corresponding to possible assignments to the other variables in the constraint. One of the efficiencies typically found in specialised propagators is the (typically implicit) use of short supports: by examining a subset of the variables, they can infer support for all other variables and values and save substantial work.

For example, consider the element([x0, x1, x2], y, z) constraint, with x0, x1, x2, y ∈ {0 . . . 2}, z ∈ {0 . . . 3}. The constraint is satisfied iff xy = z (i.e. the element in position y of vector X equals z). Consider the set of literals S1 = {x0 ↦→ 1, y ↦→ 0, z ↦→ 1}. This set clearly satisfies the definition of the constraint xy = z, but it does not contain a literal for each variable. Any extension of S with valid literals for variables x1 and x2 is a support. We call S a short support. As a second example, the watched literal propagation algorithm in SAT exploits short supports containing one variable, requiring only two such supports for a constraint of any length.

To date, general-purpose propagation algorithms rely upon supports involving all variables. In this paper, we demonstrate how to employ short supports in a new general-purpose propagation algorithm called SHORTGAC. As we will demonstrate, the use of short supports significantly improves the performance of SHORTGAC versus existing general-purpose propagation algorithms. In some cases, SHORTGAC even approaches the performance of special-purpose propagators.

2 Supports, Short Supports and GAC

A literal x ↦→ v is valid if v is in the current domain of x. The scope of a constraint c is the subset of variables that it constrains. A valid tuple for constraint c is a set of literals that contains a valid literal for each variable in the scope of c and satisfies c. With respect to a constraint c, a support for a literal l is a valid tuple for c that contains l.

Each short support is a set of literals that contains a valid literal for each of some subset of variables in the scope of c, and such that every superset of this containing one valid literal for each variable in c is a support. For example, even the empty set is a possible short support, if every remaining tuple of valid literals satisfies c (in which case c is 'entailed'.)

The property commonly established by constraint propagation algorithms is generalised arc consistency (GAC) [Mackworth, 1977]. A constraint c is GAC if and only if there exists a support for every valid literal of every variable in the scope of c. GAC is established by identifying all literals x ↦→ v for which no support exists and removing v from the domain of x.

A GAC propagation algorithm is usually situated in a systematic search. Hence, it must operate in three contexts: initialisation (at the root node), where support is established from scratch; following the deletion of one or more domain values (as a result of a branching decision and/or the propagation of other constraints), where support must be re-established selectively; and upon backtracking, where data structures must be restored to the correct state for this point in search. Our primary focus will be on the second context, operation following value deletion, although we will discuss the other two briefly.

A GAC propagation algorithm would typically be called for each deleted domain value in turn. Once the algorithm has been called for each such domain value, the constraint will be GAC. However, the propagation algorithm proposed here need not be called for every deleted domain value to establish GAC. In this paper we say that propagators attach and remove triggers on literals. When a domain value v for variable x is deleted, the propagator is called if and only if it has a trigger attached to the literal x ↦→ v.

3 SHORTGAC: An Overview

This section summarises the key ideas of the SHORTGAC propagation algorithm, along with an illustrative example.

SHORTGAC maintains a set of short supports sufficient to support all valid literals of the variables in the scope of the constraint it is propagating. We refer to these as the active supports. The major contribution of the algorithm is the efficient storage and update of the set of active supports. This efficiency rests on exploiting the observation that, using short supports, support can be established for a literal in two ways. First, as usual, a short support that contains a literal supports that literal. Second, a literal x ↦→ v is supported by a short support that contains no literal of variable x. Hence, the only short supports that do not support x ↦→ v are those which contain a literal x ↦→ w for some other value w ̸= v.

The following counters are central to the operation of the SHORTGAC algorithm:

numSupports is the total number of active supports.

supportsPerVar[x] is an array indicating the number of supports containing each variable x.

supportsPerLit[x, v] is a 2-dimensional array indicating the number of supports containing each literal x ↦→ v.

If the number of supports containing some variable x is less than the total number of supports then there exists a support s that does not contain x. Therefore, as noted, s supports all literals of x. The algorithm spends no time processing variables all of whose literals are known to be supported in this way. Only for variables involved in all supporting tuples do we have to seek support for literals with no current supports.

To illustrate, we consider the element example. Suppose in the current state SHORTGAC is storing just one support:

All valid literals are now supported. Nothing further need be done until a change in state, such as the removal of a value by propagation, or a change in state following backtracking.

4 SHORTGAC: Details

The key tasks are: counter update; iteration over variables where supportsPerVar equals numSupports; and iteration over the unsupported values of a variable. The following data structures allow us to do each of these tasks efficiently.

A short support is represented by a struct. It may be contained in multiple doubly-linked lists simultaneously (one for each literal x ↦→ v in the support). Hence, it has multiple previous and next pointers. The support struct contains:

• prev[x] An array of previous pointers, indexed by variable.
• next[x] An array of next pointers, indexed by variable.

literals An array of literals

The doubly-linked lists are accessed via supportListPerLit[x, v], an array of pointers to supports. If an active support S contains a literal x ↦→ v, then S is contained in the doublylinked list supportListPerLit[x, v]. Hence, it is possible to iterate through all supports containing any particular literal.

The algorithm iterates over all variables x where supportsPerVar[x] equals numSupports. The following data structure represents a partition of the variables by the number of supports. It allows constant time size checking and linear-time iteration of each cell in the partition, and allows any variable to be moved into an adjacent cell (ie if the number of supports increases or decreases by 1) in constant time. It is inspired by the indexed dependency array in [Schulte and Tack, 2010].

varsPerSupport is an array containing a permutation of the variables. Variables are ordered by their number of supports (supportsPerVar[x]) in ascending order.

varsPerSupInv is the inverse mapping of varsPerSupport. supportNumPtrs is an array of integers such that supportNumPtrs[i] is the smallest index in varsPerSupport with i or more supports. Therefore varsPerSupport[supportNumPtrs[i]..supportNumPtrs[i + 1]-1] contains exactly the set of variables with i supports.

Procedure swap(xi, xj) (used later) locates and swaps the two variables in varsPerSupport, also updating varsPerSupInv.

For a variable x with supportsPerVar[x] = numSupports, SHORTGAC iterates over the values with zero supports. To avoid iterating over all values, we use a set data structure:

zeroVals[x] is a stack containing the zero values for x in no particular order.

inZeroVals[x, v] is a Boolean indicating whether value v is on the stack.

When supportsPerLit[x,v] is reduced to 0, if inZeroVals[x,v] is false then v is pushed onto zeroVals[x]. As an optimisation, values are not eagerly removed from the set; they are only removed when the set is iterated. Also, the set is not backtracked. During iteration, a non-zero value is removed by swapping it to the top of the stack, and popping.

4.1 Adding and Deleting Supports

When a support is added or deleted, all the data structures described above are updated. This is done by the addSupport and deleteSupport procedures. AddSupport is given in Algorithm 1. For each literal in the support sup, sup is added to the appropriate supportListPerLit, and the two counters supportsPerVar and supportsPerLit are incremented. xi must also be moved to the next cell in varsPerSupport. Line 6 finds the end of the cell that xi is in. Line 7 swaps xi to the end of its cell, and line 8 moves a cell boundary such that xi is now in the higher cell. Lines 9-10 add a trigger to xi ↦→ a if sup is the only active support to contain that literal (otherwise xi ↦→ a will already have a trigger).

The procedure deleteSupport is similar with the following changes. On lines 3, 4 and 11, counters are decremented.

Algorithm 1 Add Support: addSupport(sup)

Require: sup: a support struct

• 1: for all (xi ↦→ a) in sup.literals do
• 2: Add sup to supportListPerLit[xi, a]
• 3: supportsPerVar[xi]← supportsPerVar[xi]+1
• 4: supportsPerLit[xi,a]← supportsPerLit[xi,a]+1
• 5: sPV←supportsPerVar[xi]
• 6: cellend ←supportNumPtrs[sPV]-1
• 7: swap(xi, varsPerSupport[cellend])
• 8: supportNumPtrs[sPV]←supportNumPtrs[sPV]-1
• 9: if supportsPerLit[xi,a]=1 then
• 10: attachTrigger(xi ,a)
• 11: numSupports←numSupports+1

On line 2, sup is removed from the list (in constant time). Lines 6-8 are altered to move xi into the lower adjacent cell in varsPerSupport. Line 6 finds the start of the cell that xi is in (supportNumPtrs[sPV+1]), line 7 remains the same and line 8 increments the lower boundary (supportNumPtrs[sPV+1]) so that xi is now in the adjacent cell. Lines 9-10 call removeTrigger if supportsPerLit[xi,a]=0. Between lines 8 and 9, a new section is added: if supportsPerLit[xi,a]=0, then value a is added to zeroVals[xi] if not already present.

All changes to data structures (except where noted above) are stored on a stack; addSupport and deleteSupport are used to revert changes upon backtracking.

4.2 The Propagation Algorithm

The SHORTGAC propagator (Algorithm 2) is only invoked when a literal contained in one or more active supports is pruned. It first calls deleteSupport for all active supports containing the pruned literal. Then it iterates through all variables xj where supportsPerVar[xj]=numSupports (lines 3-4). xj may have unsupported values. SHORTGAC iterates through zeroVals[xj], discarding values with support (lines 6-7), and seeking a new support for those without (lines 10-16).

A new support is sought by calling findNewSupport(xj , a). This returns a support for the literal if one exists. If there is no support, the literal is pruned. If there exists a support (sup) it is added on line 14. sup must support xj ↦→ a, but it does not have to contain xj ↦→ a. a is removed from zeroVals[xj] only if sup contains xj ↦→ a. At this point, numSupports and supportNumPtrs have changed, so the loop (lines 3-17) is restarted (line 17) using a goto statement. The aim is to process all variables where supportsPerVar[xj]=numSupports; adding a new support changes this set of variables, therefore the loop is restarted.

Complexity analysis of the algorithm is left for future work, and we do not claim optimality. In particular the algorithm can process variables where each value is supported. To initialise the propagation process, lines 3-17 of Algorithm 2 are invoked.

4.3 Instantiation of findNewSupport

Similarly to GAC-Schema [Bessi`ere and R´egin, 1997], SHORTGAC must be instantiated with a findNewSupport function. The function takes a valid literal, and returns a support if one exists, otherwise returns null. A findNewSupport function

Require: var, val (where val has been pruned from var) 1: while supportListPerLit[var, val] ̸= null do 2: deleteSupport(supportListPerLit[var, val]) 3: for all i ∈ {supportNumPtrs[numSupports]. . . supportNumPtrs[numSupports+1]-1} do 4: xj ←varsPerSupport[i] 5: for all a ∈ zeroVals[xj ] do 6: if supportsPerLit[xj , a] > 0 then 7: Remove a from zeroVals[xj ] 8: else 9: if a ∈ Dom(xj) then 10: sup←findNewSupport(xj , a) 11: if sup=null then 12: prune(xj ,a) 13: else 14: addSupport(sup) 15: if supportsPerLit[xj , a] > 0 then 16: Remove a from zeroVals[xj ] 17: Goto 3

may be written for a particular constraint. In the case studies below we briefly summarise what this function does.

Alternatively, we provide a generic instantiation named findNewSupport-List (Algorithm 3) that takes a list of short supports for each literal (supportList). This is analogous to the Positive instantiation of GAC-Schema [Bessi`ere and R´egin, 1997]. FindNewSupport-List has persistent state: listPos, an array of integers indexed by variable and value, initially 0. This indicates the current position in the supportList. ListPos is not backtracked. The algorithm simply iterates through the list of supports, seeking one where all literals are valid. Using listPos stops the algorithm repeatedly iterating through the first section of the list when called repeatedly. Note that a constraintspecific findNewSupport can sometimes find shorter supports than findNewSupport-list. This is because a specific findNewSupport can take advantage of current domains whereas the supportList may only contain supports given the initial domains. For example, if the constraint becomes entailed, the specific findNewSupport can return the empty support. We exploit this fact in case study 3 below.

As an optimisation, we omit literals from sup for assigned variables. This is applied to all findNewSupport functions (except for SHORTGAC-longsupport, described below).

5 Experimental Setup

The Minion solver 0.10 [Gent et al., 2006a] was used for experiments, with our own additions. We used an 8-core machine with 2.27GHz Intel Xeon E5520 CPUs and 12GB memory. All times are a median of 5 runs. We report complete run times, i.e. we have not attempted to measure the time attributable to the given propagator. This both simplifies our experiments and has the advantage that we automatically take account of all factors affecting runtime.

For each case study, we implemented a findNewSupport method for SHORTGAC specific to the constraint. We also used the generic list instantiation for comparison where possible. We compare SHORTGAC against the special-purpose propagator (when available). We also compare against SHORTGAC-longsupport (SHORTGAC with full length supports), and against GAC-Schema [Bessi`ere and R´egin, 1997] as the closest equivalent algorithm without short supports. Our implementation of GAC-Schema is very similar to SHORTGAC, using the same data structures where possible. GAC-Schema and SHORTGAC-longsupport use the same (constraint-specific) findNewSupport as SHORTGAC, and subsequently extend the short support to full length using the minimum value for each extra variable. In each case, the constraint can be compactly represented as a disjunction. Therefore we compare SHORTGAC against Constructive Disjunction. The algorithm used is based upon [Lagerkvist and Schulte, 2009], without entailment detection. We do not compare to table constraints (eg [Gent et al., 2007]) because the constraints are too large. For example, the smallest element constraints reported below have 638 valid tuples, making it impossible even to generate and store the list of allowed tuples.

6 Case Study 1: Element

We use the quasigroup existence problem QG3 [Colton and Miguel, 2001] to evaluate SHORTGAC on the element constraint. The problem class has one parameter n, specifying the size of an n × n table (qg) of variables with domains {0 . . . n}. Rows, columns and one diagonal have GAC allDifferent constraints, following Colton and Miguel's model. The element constraints represent the QG3 property that (i ∗ j) ∗ (j ∗ i) = i. This translates as ∀i, j : element(qg, aux[i, j], i), and aux[i, j]= n × qg[i, j] + qg[j, i], where aux[i, j] has domain {0 . . . n × n - 1}.

For the constraint element(X, y, z), the findNewSupport method for SHORTGAC returns tuples of the form 〈xi ↦→ j, y ↦→ i, z ↦→ j〉, where i is an index into the vector X and j is a common value of z and xi. SHORTGAC-list has all supports of this form. For Constructive Or, we used (x0 = z ∧ y = 0) ∨ · · · ∨ (xn = z ∧ y = n).

We searched for all solutions, with limits of 100,000 nodes, 1,800 seconds, and 12GB of virtual memory. Table 1 shows our results on QG3. Of the general purpose methods, using short supports in either functional or list form is dramatically better than any alternative. For example at n = 10, even the

Algorithm 3 findNewSupport-list: findNewSupport(xi, a)

Require: xi, a, supportList 1: for all j ∈ {listPos[xi, a]. . .(supportList[xi, a].size-1)} do 2: sup ←supportList[xi, a, j] 3: if all literals in sup are valid then 4: listPos[xi, a]← j 5: return sup 6: for all j ∈ {0 . . .listPos[xi, a]-1} do 7: sup ←supportList[xi, a, j] 8: if all literals in sup are valid then 9: listPos[xi, a]← j 10: return sup 11: return null

slower, list based method is 200 times faster than Constructive Or, the best of the other methods. Functional SHORTGAC is about twice as fast as SHORTGAC-list, but cannot compete with the special purpose element propagator in Minion [Gent et al., 2006b] which is about 5-9 times faster. It remains clear that exploiting short supports is very beneficial compared to other general purpose methods.

7 Case Study 2: Lex-ordering

We use BIBD problems to evaluate SHORTGAC on the lexicographic ordering constraint. The lex constraint is placed on both the rows and columns, to perform the "Double Lex" symmetry breaking method. We use the BIBD model and GACLex propagator given by [Frisch et al., 2002]. We use BIBDs with the parameter values (4n + 3, 4n + 3, 2n + 1, 2n + 1, n) and we impose a 2GB limit on runs. All methods explore identical search spaces. We searched for all solutions up to a node limit of 1,000,000 or time limit of 1800s (whichever was first). This limits all instances except n = 3 which required 41,982 nodes.

For the constraint lexleq(X, Y ), we define mxi = min(Dom(xi)) and myi = max(Dom(yi)). The findNewSupport method for SHORTGAC finds the lowest index i ∈ {0 . . . n} such that mxi < myi, or i = n. The case i = n arises when X cannot be lex-less than Y , so a support is sought for X = Y . If i < n, the support contains xi ↦→mxi, yi ↦→ myi. For each index j < i, if mxj = myj, then the short support contains xj ↦→mxj, yj ↦→myj otherwise there is no valid support and null is returned.

The lex constraint on two arrays of length n and domain size d has more than dn short supports since all assignments where the two arrays are equal satisfy the constraint and cannot be reduced. SHORTGAC-list is not practical for any substantial constraint. Constructive Or uses the following representation: (x0 < y0) ∨ (x0 = y0 ∧ x1 < y1) ∨ · · · , including the case where all pairs are equal.

Table 2 shows the results of our experiments on non-list based methods with values of n from 3 to 24. It is clear that the best method is the special purpose Lex propagator, up to twice as fast as SHORTGAC. The speedup of Lex over SHORTGAC increases only very slowly, from 1.47 at n = 3 to 2.02 at n = 24. SHORTGAC is by far the best general purpose method. At n = 3 SHORTGAC is 6.9 times better than the best alternative general-purpose method, and by n = 24 SHORTGAC is 692 times faster.

8 Case Study 3: Rectangle Packing

The rectangle packing problem [Simonis and O'Sullivan, 2008] (with parameters n, width and height) consists of packing all squares from size 1 × 1 to n × n into the rectangle of size width × height. This is modelled as follows: we have variables x1 . . . xn and y1 . . . yn, where (xi, yi) represents the cartesian coordinates of the lower-left corner of the i × i square. Domains of xi variables are {0 . . . width - i}, and for yi variables are {0 . . . height - i}. Variables are branched in decreasing order of i, with xi before yi, smallest value first. The only type of constraint is non-overlap of squares i and j: (xi +i ≤ xj) ∨(xj +j ≤ xi) ∨(yi +i ≤ yj) ∨(yj +j ≤ yi) Minion does not have the special-purpose non-overlap constraint [Simonis and O'Sullivan, 2008], so we only report a comparison of general purpose methods.

The domains of xn and yn are reduced to break flip symmetries as described in [Simonis and O'Sullivan, 2008]. Our focus is performance of the non-overlap constraint, and so we did not implement the commonly-used implied constraints.

The findNewSupport function for SHORTGAC is as follows. If any of the four disjuncts above are entailed given the current domains, return the empty support (indicating entailment). Otherwise, return a support with 2 literals to satisfy one of the four disjuncts. SHORTGAC-list has all supports of size 2.

For the experiment we used the optimum rectangle sizes reported by [Simonis and O'Sullivan, 2008]. Virtual memory was limited to 12GB. Times are given for the first 50,000 nodes of search in Table 3. We can see that SHORTGAC is by far the best technique. Of the other methods, GAC-Schema is second-best, but is always at least 5 times slower and can be almost 40 times slower. SHORTGAC-list is faster than GAC-Schema until it reaches larger problems, when it is first slightly slower and then runs out of memory. GAC-Schema in turn is significantly faster than either using SHORTGAC with full length tuples, or using Constructive Or. In summary, these results very clearly show the benefits of using short supports.

9 RelatedWork

Our use of counters to count supports is inspired by AC4 [Mohr and Henderson, 1986], and is also related to the concept of quantitative supports [Jain et al., 2010]. There has been study of compressing the tuples of a constraint (eg using tries [Gent et al., 2007]). Such techniques are orthogonal to this paper because they only assist in finding full-length supports.

Katsirelos and Walsh [2007] proposed a different generalisation of support, called a c-tuple. A c-tuple is a set of literals, such that every valid tuple contained in the c-tuple satisfies the constraint. Katsirelos and Walsh give an outline of a modified version of GAC-Schema which directly stores c-tuples. While c-tuples offer space savings when storing constraints, Katsirelos and Walsh found using c-tuples provides almost no performance improvement over GAC-Schema.

For Constructive Or, Lhomme observed that a support for one disjunct A will support all values of any variable not contained in A. The concept is similar to a short support albeit less general, because the length of the supports is fixed to the length of the disjuncts. He presents a non-incremental constructive disjunction for two disjuncts [Lhomme, 2003].

10 Conclusions

We have introduced and described in detail SHORTGAC, a general purpose propagation algorithm for short supports. Either it can be given a specialised function to find new supports for each constraint, or used with a method which accepts an explicit list of short supports. In three case studies, SHORTGAC is far faster than general purpose methods. In the best case it achieved speeds about 50% of that of a special purpose propagator. We conclude that where short supports are available, SHORTGAC will provide much better performance than existing general-purpose constraint propagation methods.

We identify two areas of interest for future work. First, we observed that SHORTGAC with lists has memory problems. Providing a practically effective version of the table constraint with short supports would further increase the utility of our work. Second, we see that SHORTGAC with full length supports was significantly slower than GAC-Schema. It would be beneficial if a single propagation algorithm could be found that was as fast as SHORTGAC on short supports and as fast as GAC-Schema on long supports.

Acknowledgements

We would like to thank anonymous reviewers for their comments, and EPSRC for funding this work through grants EP/H004092/1 and EP/E030394/1.