Generalized support and formal development of constraint propagators

Abstract

Constraint programming is a family of techniques for solving combinatorial problems, where the problem is modelled as a set of decision variables (typically with finite domains) and a set of constraints that express relations among the decision variables. One key concept in constraint programming is propagation: reasoning on a constraint or set of constraints to derive new facts, typically to remove values from the domains of decision variables. Specialized propagation algorithms (propagators) exist for many classes of constraints.

The concept of support is pervasive in the design of propagators. Traditionally, when a domain value ceases to have support, it may be removed because it takes part in no solutions. Arc-consistency algorithms such as AC2001 [in: Proceedings 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), 2001, pp. 309–315] make use of support in the form of a single domain value. GAC algorithms such as GAC-Schema [in: Proceedings 15th International Joint Conference on Artificial Intelligence (IJCAI 97), 1997, pp. 398–404] use a tuple of values to support each literal. We generalize these notions of support in two ways. First, we allow a set of tuples to act as support. Second, the supported object is generalized from a set of literals (GAC-Schema) to an entire constraint or any part of it.

We design a methodology for developing correct propagators using generalized support. A constraint is expressed as a family of support properties, which may be proven correct against the formal semantics of the constraint. We show how to derive correct propagators from the constructive proofs of the support properties. The framework is carefully designed to allow efficient algorithms to be produced. Derived algorithms may make use of dynamic literal triggers or watched literals [in: Proc. 12th International Conference on the Principles and Practice of Constraint Programming (CP 2006), 2006, pp. 182–197] for efficiency. Finally, three case studies of deriving efficient algorithms are given.

Keywords

Constraint satisfaction problem constraint programming formal methods

1. Introduction

In this paper we provide a formal development of the notion of support in constraint satisfaction. This notion is ubiquitous and plays a vital role in the understanding, development, and implementation of constraint propagators, which in turn are the keystone of a successful constraint solver. While we focus on a formal development in this paper, our purpose is not to describe formally what is currently seen in constraint satisfaction. Instead, we generalize the notion of support so that it can be used in a wider variety of propagators. The result is the first step in a twin programme of developing a formal understanding of constraint algorithms, while also developing notions such as generalized support which should lead to improved constraint algorithms in the future.

The methodology presented here for formal development of propagators is based on the proofs-as-programs and propositions-as-types interpretations of constructive type theory [11,17]. Like the earlier development in [9], the approach presented here uses a constructive type theory as the formal framework for specifying and developing programs. There, the proofs were mechanically checked in the Nuprl theorem prover [12], here the development is formal but proofs have not been mechanically checked.

The paper is structured as follows. In this section, we introduce the key concepts used in our method and give an overview of related work. In Section 2 we define the basic mathematical concepts used in the rest of the paper. In Section 3 we define generalized support and present the method for development of constraint propagators that are correct by construction. In Section 4 we present three case studies where we apply our method. In the third case study we develop and implement a new propagator that can be more efficient than the existing propagator in a popular constraint solver. Finally we conclude in Section 5.

1.1. Overview of the constraint satisfaction problem

A constraint is simply a relation over a set of variables. Many different kinds of information can be represented with constraints. The following are simple examples: one variable is less than another; a set of variables must take distinct values; task A must be scheduled before task B; two objects may not occupy the same space. It is this flexibility which allows constraints to be applied to many theoretical, industrial and mathematical problems.

The classical constraint satisfaction problem (CSP) has a finite set of variables, each with a finite domain, and a set of constraints over those variables. A solution to an instance of CSP is an assignment to each variable, such that all constraints are simultaneously satisfied – that is, they are all true under the assignment. Solvers typically find one or all solutions, or prove there are no solutions. The decision problem (‘does there exist a solution?’) is NP-complete [1], therefore there is no known polynomial-time procedure to find a solution.

1.2. Solving CSP

Constraint programming includes a great variety of domain specific and general techniques for solving systems of constraints. Since CSP is NP-complete, most algorithms are based on a search which potentially explores an exponential number of nodes. The most common technique is to interleave splitting and propagation. Splitting is the basic operation of search, and propagation simplifies the CSP instance. Apt views the solution process as the repeated transformation of the CSP until a solution state is reached [1]. In this view, both splitting and propagation are transformations, where propagation simplifies the CSP by removing domain values that cannot take part in any solution. A splitting operation transforms a CSP instance into two or more simpler CSP instances, and by recursive application of splitting any CSP can be solved.

Systems such as Choco [21], IBM ILOG CPLEX CP Optimizer [18] and Minion [14,15] implement highly optimized constraint solvers based on search and propagation, and (depending on the formulation) are able to solve large problem instances quickly.

Our focus in this paper is on propagation algorithms. A propagation algorithm operates on a single constraint, simplifying the containing CSP instance by removing values from variables in the scope of the constraint. Values which cannot take part in any solution are removed. For example, a propagator for $x ⩽ y$ might remove all values of x which are greater than the largest value of y. Typically propagation algorithms are executed iteratively until none can make any further simplifications.

1.3. Proofs to propagators

Researchers frequently invent new algorithms and (sometimes) give proofs of correctness, of varying rigour. In this paper we provide a formal semantics of CSP. This allows us to formally characterize correctness of constraint propagators, and therefore aid the proof of correctness of propagators. Following this, we lay the groundwork for automatic generation of correct propagators. The method is to write a set of support properties which together characterize the constraint. Each property is inserted into a schema, and a constructive proof of the schema is generated. This proof is then translated into a correct-by-construction propagator. This method is based on the concept of generalized support, described in the next section. Finally, we give examples of this method by deriving propagators for the element, occurrenceleq and occurrencegeq constraints.

1.4. Generalized support

Central to this work is the notion of support. This notion is used informally in many places (for example, in the description of the algorithm GAC-Schema [7]) and more formally by Bessière [5]. We generalize the concept of support, and develop a formal framework to allow us to produce rigorous proofs of the correctness of propagators that exploit the generalized concept of support.

Support is a natural concept in constraint programming. Constraint propagators remove unsupported values from variable domains, thus simplifying a CSP instance. Supported values cannot be removed, since they may be contained in a solution. Thus a support is evidence that a value (or set of values) may be contained in a solution. If no support exists, it is guaranteed that a value (or set of values) is not contained in any solution.

A support property characterises the supports of a particular value (or set of values) for a particular constraint. For example, three support properties of an element constraint are given by Gent et al. [15]. Each of these three properties is used to create a propagator, such that the three propagators together achieve generalized arc consistency. In this instance, writing down support properties assisted in proving the propagators correct.

We show that correct support properties can be used to create propagators that are correct by construction. We describe a general propagation schema, which is a description of what should be proved when support is lost for a given support property. This captures how propagators work in practice. They are triggered when it is noted that the current support is lost. The propagator then seeks to re-establish support. This might be possible on the current domains, or it may need to narrow domains (i.e. remove some values of some variables), or it may be that no new support is possible and the constraint is guaranteed to be false. The propagation schema specialized for a given support property can be proven constructively. The proof contains sufficient information to be translated into a correct propagator. We envisage two main uses for such a propagator. For some constraints, it may be an efficient propagator that can be used directly. Otherwise, the constructed propagator may be used as part of an informal argument for the correctness of an efficient propagator.

1.5. Related work

There are a number of items of related work with related or similar goals, however the approach taken in each case is quite different to our approach. Apt and Monfroy [2] generate propagation rules such as $X = s \to y \neq a$ , where X is a vector of CSP variables, s is a vector of values within the initial domain of X, y is a CSP variable and a is a value in the initial domain of y. Rules correspond directly to propagation in a constraint solver (i.e. when X is assigned s, a is removed from the domain of y). A set of rules is generated for a given constraint by a search over the (potentially very large) space of possible rules. In contrast, our approach is much broader in that it is not restricted to generating implication rules. Our framework allows both the derivation of new propagators and proof of correctness of existing ones.

Van Hentenryck, Saraswat and Deville [27] designed indexicals, a high-level language for implementing propagators. Indexicals allow straightforward and transparently correct implementations of propagators for simple constraints, however there is no way to implement sophisticated propagators for global constraints using indexicals. Tack, Schulte and Smolka [26] presented a specification language for constraints on finite set variables, and an implementation language called set projectors that is inspired by indexicals. They present a method to automatically translate specifications into set projectors. Our approach is much broader than either indexicals or set projectors, since both restrict the form of propagation algorithms that can be implemented.

Beldiceanu, Carlsson and Petit [4] describe constraints using finite state automata extended with counters. For a constraint C, the automaton for C can check whether any given assignment satisfies C. Beldiceanu, Carlsson and Petit give a method to translate an automaton into a set of short constraints (a decomposition) such that propagating them will propagate the original constraint C, and there are (in some cases) guarantees of the strength of propagation. The approach has been subsequently refined, for example by linking overlapping prefixes and suffixes of constraints [3]. Their approach generates decompositions of a particular form, whereas in this paper our focus is on deriving efficient propagators.

Cohen, Jefferson and Petrie [10,19] studied the properties of triggers, in particular comparing static triggers with movable triggers on a number of constraint classes and consistencies. They prove lower bounds on the number of triggers required, showing in most cases that many more static triggers are required compared to movable triggers. To do this they generalise the concept of support in a similar way to us, however their work treats each propagator as a monolithic black box whereas we are interested in constructing propagators and proving correctness and other properties of them.

2. Definitions and notation

2.1. The standard mathematical account

We start by giving the standard definition of a constraint satisfaction problem (e.g. see [5,13]). Formal definitions of the notations used here are given below.

Definition 1 (Constraint Satisfaction Problem).

A Constraint Satisfaction Problem (CSP) is given by a triple $⟨ X, σ, C ⟩$ where X is a k-tuple of variables $X = ⟨ x_{1}, \dots, x_{k} ⟩$ and σ is a signature (a function $σ : X \to 2^{Z}$ mapping variables in X to their corresponding domains, such that $σ (x_{i}) ⊊ Z$ is the finite domain of variable $x_{i}$ ). C is a tuple of extensional constraints $C = ⟨ C_{1}, \dots, C_{m} ⟩$ where each $C_{i}$ is of the form $⟨ Y, R_{Y} ⟩$ where $Y \subseteq X$ is a tuple of variables called the schema or scope of the constraint $C_{i}$ . Also, $R_{Y}$ is a relation given by a subset of the Cartesian products of the domains of the variables in the scope Y and is called the extension of $C_{i}$ .

Definition 2 (Satisfying tuple).

We say a Z-tuple τ satisfies constraint $⟨ Y, R_{Y} ⟩$ if $Y \subseteq Z$ , and the projection $Y [τ]$ is in $R_{Y}$ (i.e. if the projection of the scope Y from τ is in $R_{Y}$ ).

Definition 3 (Solution).

A solution to a CSP $⟨ X, σ, C ⟩$ is a tuple τ, with schema X, such that τ satisfies every constraint in C.

2.2. Variable naming conventions, ranges, and literals

We use lower case letters (possibly subscripted or primed) from near the end of the Latin alphabet ${w, x, y, z}$ to denote variables. We use Latin letters ${i, j, k}$ to denote integer indexes, and use the Latin letters occurring early in the alphabet ${a, b, c, d}$ (possibly subscripted) to denote arbitrary integer values.

Ranges are defined as follows. $\begin{matrix} {b \dots c} \overset{def}{=} {a \in Z ∣ b ⩽ a \land a ⩽ c} \end{matrix}$ We write $2^{A}$ to denote the powerset (set of all subsets) of A. A literal is a variable-value pair (e.g. $⟨ x, 5 ⟩$ ).

2.3. Vectors

We use uppercase letters $W, X, Y, Z, \dots$ to denote vectors of variables. We use the Greek letters ${τ, τ^{'}, τ_{1}, τ_{2}, \dots}$ to denote tuples of integer values.

We write finite vectors as sequences of values enclosed in angled brackets, (e.g. $⟨ x, y, z ⟩$ ). The empty vector is written $⟨ ⟩$ . We take the operation of prepending a single element to the left end of a vector as primitive and denote this operation $x \cdot Y$ . We abuse this notation by writing $X \cdot Y$ for the concatenation of vectors X and Y. We write $| Y |$ to denote the length of vector Y. Given a vector Y, we write $Y [i]$ to denote the (zero-based) ith element of Y. This operation is undefined if $i \notin {0 \dots | Y | - 1}$ .

Membership in a vector is defined as follows. $\begin{matrix} z \in Y \overset{def}{=} \exists i \in {0 \dots | Y | - 1} . Y [i] = z \end{matrix}$ We will sometimes need to collect the set of indexes to an element in a vector. $\begin{matrix} Y [[z]] \overset{def}{=} {i \in {0 \dots | Y | - 1} ∣ Y [i] = z} \end{matrix}$ Thus, $⟨ x, y, z, x ⟩ [[x]] = {0, 3}$ . Note that $Y [[z]] \neq \emptyset$ iff $z \in Y$ and also each index in $Y [[z]]$ is a witness for $z \in Y$ .

If $y \in Y$ , we write $Y - y$ to denote the vector obtained from Y by deleting the leftmost occurrence of y from Y. $Y - y = Y$ if $y \notin Y$ . We write $Z - Y$ for the vector obtained by removing leftmost occurrences of all ( $y \in Y$ ) from Z. Given a vector Z, we write ${Z}$ to denote the set of elements in Z and given a set of variables S we write $⟨ S ⟩$ to denote a vector of the variables in S; the reader may assume the variables in $⟨ S ⟩$ occur in increasing lexicographic order. Intersection and union are defined on vectors by taking them as sets: $X \cap Y \overset{def}{=} ⟨ {X} \cap {Y} ⟩$ ; and $X \cup Y \overset{def}{=} ⟨ {X} \cup {Y} ⟩$ . We write $Y \subseteq X$ to mean ${Y} \subseteq {X}$ , i.e. that every element in Y is in X with no stipulations on relative lengths of X or Y or on the order of their elements.

2.4. Signatures

A signature σ is a function mapping variables in X to their associated domains. Thus, signatures are functions $σ : X \to 2^{Z}$ where in practice, the subset of integers mapped to is finite. Where σ and $σ^{'}$ are signatures mapping variables in X to their finite integer domains: $\begin{matrix} σ^{'} ⊑_{X} σ \overset{def}{=} \forall x \in X . σ^{'} (x) \subseteq σ (x) \end{matrix}$ We write $σ^{'} ⊏_{X} σ$ if $σ^{'} ⊑_{X} σ$ and $\exists x \in X : σ^{'} (x) ⊊ σ (x)$ , i.e. if some domain of $σ^{'}$ is a proper subset of the corresponding domain of σ. We drop the schema subscript when the schema is clear from the context. We state the following without proof.

Lemma 1 (Signature Inclusion Well-founded).

The relation ⊏ is well-founded if restricted to signatures with finite domains.

2.5. Relations

In the description of a CSP given above, a constraint $⟨ Y, R_{Y} ⟩$ is a relation where the schema Y gives the variable names and $R_{Y}$ is the set of tuples in the relation.

Given a signature σ mapping the variables in schema Y to their domains, a relation $⟨ Y, R_{Y} ⟩$ is well-formed with respect to σ iff the following conditions hold:

All tuples in $R_{Y}$ have length $| Y |$ ;

The values in each column come from the specified domain for that column: $\begin{matrix} \forall τ \in R_{Y} . \forall i \in {0 \dots | Y | - 1} . τ [i] \in σ (Y [i]) \end{matrix}$

Schemata are vectors of variable names with no restriction on how many times a variable may occur. Thus it is possible to have a wellformed relation whose schema has common names for multiple columns. Given a signature σ over a schema X, a tuple τ is called a X-tuple if $⟨ X, {τ} ⟩$ is well-formed w.r.t. σ. In this case, we write $X - {tuple}_{σ} (τ)$ . We write $X - {tuple}_{σ}$ for the set of tuples satisfying this condition.

2.5.1. Tuple coherency

Conceptually, relations provide a representation for storing valuations (assignments of values to variables) and so we must distinguish between tuples which represent coherent valuations (even when their schemata may contain duplicate variable names) and tuples that do not. This motivates the following definitions.

The wellformedness condition on relations requires values in columns labeled by a variable come from the domain of that variable, but does not rule out cases where a single tuple with multiple columns named by the same variable have different values in those columns.

Example 1.
Consider the relation $\begin{matrix} ⟨ ⟨ x, x, y ⟩, {⟨ 1, 2, 3 ⟩, ⟨ 1, 1, 3 ⟩, ⟨ 2, 2, 3 ⟩} ⟩ \end{matrix}$ The variable x occurs twice in the schema and the first tuple in the schema assigns different values to x, this tuple is not coherent.

An X-tuple τ is coherent w.r.t. variable z iff the following holds. $\begin{matrix} coh {X, z} (τ) \overset{def}{=} \forall i, j \in X [[z]] . τ [i] = τ [j] \end{matrix}$ We say a tuple is incoherent w.r.t. z if it is not coherent. Note that this definition is sensible whether $z \in X$ or not. A simple consequence of the definition is that an X-tuple τ is incoherent w.r.t. variable z iff $\begin{matrix} \exists i, j \in X [[z]] . τ [i] \neq τ [j] \end{matrix}$ An X-tuple τ is coherent with schema Y iff it is coherent w.r.t. all variables $z \in Y$ . $\begin{matrix} coh {X, Y} (τ) \overset{def}{=} \forall z \in Y . coh {X, z} (τ) \end{matrix}$ We say an X-tuple is incoherent with respect to schema Y if it is not coherent w.r.t. Y. Only coherent tuples count as solutions (Definition 3). Remark 1.
In many constraint solvers, incoherent tuples may arise during a computation, but they are never counted among solutions. For example, the Global Cardinality constraint $\begin{matrix} GCC (⟨ x, x, y ⟩, ⟨ 1, 2 ⟩, ⟨ (2 \dots 3), (1 \dots 2) ⟩) \end{matrix}$ (stating that value 1 occurs two or three times, and value 2 occurs once or twice among variables $⟨ x, x, y ⟩$ ) could generate the incoherent tuple $⟨ 1, 2, 1 ⟩$ internally when using Règin’s algorithm [23].1
¹
Règin’s algorithm [23] is polynomial-time and enforces GAC iff the schema contains no duplicate variables. With duplicate variables, enforcing GAC on GCC is NP-Hard [6], therefore it is sensible to use Règin’s algorithm in this case even though it will not enforce GAC.

Generating incoherent tuples affects both the internal state of a constraint propagator, and the number of vertices in the search tree.

Strictly speaking, because incoherent tuples do not count as solutions, the semantics could be specified simply disallowing them. However, this approach would rule out faithful finer grained representations of the internal states of constraint solvers which do generate incoherent tuples, for example when searching for support. Based on this, we have decided to include them although this adds some complexity to the specification.

2.5.2. Selection

Selection is an operation mapping relations to relations generating new ones from old by filtering rows (tuples) based on predicates on the values in the tuple.

Given a relation $⟨ Y, R_{Y} ⟩$ and an index $i \in {0 \dots | Y | - 1}$ , and a value (say a), index selection is defined as follows. $\begin{matrix} {select}_{(i = a)} (R_{Y}) \overset{def}{=} {τ \in R_{Y} ∣ τ [i] = a} \end{matrix}$

The tuples selected from a relation by index selection are not guaranteed to be coherent with respect to schema Y.

Given a relation $⟨ Y, R_{Y} ⟩$ , a variable x, and a value a, value selection is defined as follows. $\begin{array}{l} {select}_{(x = a)} (R_{Y}) \\ \overset{def}{=} {τ \in R_{Y} ∣ \forall i \in Y [[x]] . τ [i] = a} \end{array}$

Thus a tuple τ is included in a selection ${select}_{(x = a)} R_{Y}$ if and only if all columns of τ indexed by x have value a, i.e. τ must be coherent for x and those columns must have value a.

Lemma 2 (Selection Wellformed).

For all well-formed relations $⟨ Y, R_{Y} ⟩$ and all x, and all $a \in Z$ , the relation $⟨ Y, {select}_{(x = a)} R_{Y} ⟩$ is well-formed.

Finally, we define coherent selection as follows. $\begin{matrix} {select}_{Y} (R_{X}) \overset{def}{=} {τ \in R_{X} ∣ coh {X, Y} (τ)} \end{matrix}$ Coherent selection selects the tuples which are coherent with respect to Y.

2.5.3. Projection

Projection is an operation for creating new relations from existing ones by allowing for the deletion, reordering and duplication of columns. We use a generalized version here that allows duplicate names. This is because many constraint solvers (including Minion [14] for example) allow schemata to contain duplicate names.

Lemma 3 (Projection maps exist).

For all vectors X and Y, if $Y \subseteq X$ , then there exists a function from the indexes of Y to the indexes of X ( $f \in {0 \dots | Y | - 1} \to {0 \dots | X | - 1}$ ) such that $\begin{matrix} \forall i \in {0 \dots | Y | - 1} . Y [i] = X [f (i)] \end{matrix}$

Note that there is no restriction on the relative lengths of X and Y, e.g. it is possible for any of the following to hold: $| Y | < | X |$ , $| Y | = | X |$ or $| Y | > | X |$ . The projection maps are evidence witnessing claims of the form $Y \subseteq X$ . Furthermore, because our model allows for duplicated columns, there may be multiple projection maps witnessing an inclusion $Y \subseteq X$ .

Example 2.
Consider $\begin{matrix} Y = ⟨ x_{4}, x_{2}, x_{2}, x_{1}, x_{3} ⟩ X = ⟨ x_{1}, x_{2}, x_{3}, x_{4} ⟩ \end{matrix}$ then $Y \subseteq X$ is witnessed by the projection map: $\begin{matrix} {⟨ 0, 3 ⟩, ⟨ 1, 1 ⟩, ⟨ 2, 1 ⟩, ⟨ 3, 0 ⟩, ⟨ 4, 2 ⟩} \end{matrix}$ Similarly, $X \subseteq Y$ and is witnessed by the following $\begin{matrix} {⟨ 0, 3 ⟩, ⟨ 1, 1 ⟩, ⟨ 2, 4 ⟩, ⟨ 3, 0 ⟩} \end{matrix}$ Also $⟨ x_{2} ⟩ \subseteq Y$ is witnessed by two functions, ${⟨ 0, 1 ⟩}$ and ${⟨ 0, 2 ⟩}$ .
Lemma 4 (Tuple Projection).

Given X and Y, if $Y \subseteq X$ is witnessed by f, for each X-tuple τ there is a vector $Y_{f} (τ) : {0 \dots | Y | - 1} \to Z$ such that $\begin{matrix} \forall i \in {0 \dots | Y | - 1} . Y_{f} (τ) [i] = τ [f (i)] \end{matrix}$

Corollary 1 (Tuple Projection Wellformed).

Given X and Y, if $Y \subseteq X$ is witnessed by f, for each X-tuple τ, $Y_{f} (τ)$ is a Y-tuple, i.e. $| Y_{f} (τ) | = | Y |$ and all values in $Y_{f} (τ)$ are in their domains.

Whenever $Y \subseteq X$ , projection maps f and g witnessing this fact behave the same when used to index into tuples coherent with Y. This is illustrated by the following example.

Example 3.
Suppose $Y = ⟨ x, y ⟩$ and $X = ⟨ x, x, w, y, w ⟩$ then there are two projections maps witnessing $Y \subseteq X$ , $f = {⟨ 0, 0 ⟩, ⟨ 1, 3 ⟩}$ and $g = {⟨ 0, 1 ⟩, ⟨ 1, 3 ⟩}$ . Now, any length $| X | = 5$ tuple coherent with Y is of the form $τ = ⟨ a, a, b, c, d ⟩$ where $a, b, c, d \in Z$ . Thus, even though $f (0) \neq g (0)$ the following equalities hold: $\begin{matrix} τ [f (0)] = τ [0] = a = τ [1] = τ [g (0)] \end{matrix}$

This observation is made precise by the following lemma.
Lemma 5 (Coherent Projection Unique).

For all X and Y, and for all projection maps f and g witnessing $Y \subseteq X$ , for all X-tuples τ coherent with schema Y, $Y_{f} (τ) = Y_{g} (τ)$ .

Notational Remark 1.
Since projections Z where $Z \subseteq X$ do not depend on the projection map they are built from when the X-tuple τ is coherent with Z, we will simply write $Z (τ)$ in this case.
Lemma 6 (Projection Coherent).

For all X, Y and Z, if $Y \subseteq X$ and if τ is an X-tuple coherent with Z, then $Y [τ]$ is a Y-tuple coherent with Z.

So far we have defined projection of a single tuple, potentially with repeated variables in the schema. We lift the notation tuple-wise to relations as given by the following definition.

Definition 4 (Relation Projection).

Given X and Y, and a wellformed relation $⟨ X, R_{X} ⟩$ , if $Y \subseteq X$ is witnessed by f, $\begin{array}{l} Y_{f} (⟨ X, R_{X} ⟩) \\ = ⟨ Y, {τ \in Z^{| Y |} ∣ \exists τ^{'} \in R_{X} . τ = Y_{f} (τ^{'})} ⟩ \end{array}$

Lemma 7 (Relation Projection WF).

For all well-formed relations $⟨ X, R_{X} ⟩$ and all Y, $Y \subseteq X$ having a projection map f, the relation $Y_{f} (⟨ Y, R_{Y} ⟩)$ is well-formed.

2.5.4. Equivalence of constraints

Now that we have relation projection, we are able to define an equivalence of constraints which does not depend on the ordering (or the length) of schemata.

Definition 5 (Schema Equivalence).

$\begin{matrix} X \equiv Y \overset{def}{=} X \subseteq Y \land Y \subseteq X \end{matrix}$

Schema equivalence requires only that X and Y contain the same set of variables. The order of variables and the number of duplicates are not restricted.

Definition 6 (Constraint Equivalence).

$\begin{array}{l} ⟨ X, R_{X} ⟩ \equiv ⟨ Y, R_{Y} ⟩ \\ \overset{def}{=} X \equiv Y \\ \land Y \subseteq X is witnessed by projection map f \\ \land Y_{f} ({select}_{X} (⟨ X, R_{X} ⟩)) \\ = {select}_{Y} (⟨ Y, R_{Y} ⟩) \end{array}$

There are several steps to the constraint equivalence definition. First, it is required that the schemata are equivalent. Then we find a projection map f that will be used to reorder the schema X to match Y. Coherent selection is used to remove the incoherent tuples of both constraints. The schema X of the first constraint is reordered to match Y. Finally, the two constraints are equivalent if they have the same set of coherent tuples.

Incoherent tuples are removed before reordering the schema X, therefore any projection map f will produce the same set of reordered tuples (as in Example 3).

2.6. Syntactic definition of relations

Constraints are rarely presented extensionally but are instead described in some syntactic way. We introduce the following notation to denote the map from syntactic descriptions to their extensional meanings.

Definition 7 (Semantics).

Given a syntactic description of a constraint (say $C$ ) over schema X and where σ is a signature consistent with X, we will write ${[[C]]}_{σ}$ to denote its extension.

So, if we have a constraint $Element (X, y, z)$ where X is a vector of variables and y and z are variables, and Element has a defined meaning, we can write ${[[Element (X, y, z)]]}_{σ}$ to obtain its relation within some signature σ.

3. Propagation and support

Propagation is the process of narrowing the domains of variables so that solutions are preserved. This effectively shrinks the search-space and is one of the fundamental techniques used in constraint programming. It has been described ([13, pp. 17]) as a process of inference to distinguish it from search. Most work on propagation considers the constraints singly.

Definition 8 (Generalized Arc Consistency).

Given a constraint $C$ with schema X and a signature σ, we say $σ^{'} ⊑ σ$ is Generalized Arc Consistent iff $\begin{array}{l} \forall i \in {0 \dots | X | - 1} . \forall a \in σ (X [i]) . \\ a \in σ^{'} (X [i]) \leftrightarrow \exists τ \in {[[C]]}_{σ} . τ [i] = a \end{array}$ If $σ^{'}$ is Generalized Arc Consistent, we say it is GAC.

Corollary 2 (Generalized Arc Consistency).

Given a constraint $C$ and a signature σ, σ is GAC for $C$ iff $\begin{matrix} \forall σ^{'} ⊏ σ . {[[C]]}_{σ^{'}} \subset {[[C]]}_{σ} \end{matrix}$ i.e. if all signatures having strictly narrower domains provide strictly fewer solutions for $C$ than σ.

Enforcing GAC is the strongest form of propagation that considers constraints singly and acts only on the variable domains. Other forms of consistency (such as bound consistency) lie between GAC and no change (i.e. $σ^{'} = σ$ ).

3.1. Support

The concept of support was introduced in Section 1.4. Support is evidence that a set of domain values (or a single value) are consistent for some definition of consistency (for example, GAC) for a particular constraint C. If a set of values have no support, then they cannot be part of any solution to C, and therefore can be eliminated from variable domains without losing any solutions to the CSP. The concept of support is central to the process of propagation.

In [5, pp. 37] Bessière gives a description of when a tuple supports a literal. We use a more expressive model where support (or perhaps we should call it evidence) is defined by sets of tuples. In most cases, supports will be singletons (i.e. they are simply represented by a set containing a single tuple). However, some constraints require a set of tuples to express the condition for support.

Example 4.
Consider the AllDifferent constraint $\begin{matrix} C = AllDiff (x_{1}, x_{2}, x_{3}) \end{matrix}$ with the signature σ : $x_{1} \in {1, 2}$ , $x_{2} \in {1, 2, 3, 4}$ , $x_{3} \in {1, 2, 3, 4, 5}$ . AllDifferent means that each variable must take a distinct value. This signature is GAC. Given Bessière’s description of support [5, pp. 37] (as used by general-purpose GAC algorithms such as GAC-Schema [7]), each literal in the signature would be supported by a tuple containing the literal. Hence every literal is contained in the support for $C$ . However, not all literals are required; the following set is sufficient: $L = {⟨ x_{1}, 1 ⟩, ⟨ x_{1}, 2 ⟩, ⟨ x_{2}, 2 ⟩, ⟨ x_{2}, 4 ⟩, ⟨ x_{3}, 2 ⟩, ⟨ x_{3}, 3 ⟩, ⟨ x_{3}, 5 ⟩}$ [16, §5.2]. As long as all literals in L remain valid, in some smaller signature $σ_{1} ⊑ σ$ , then the constraint remains GAC. This can be used to avoid calling the propagator, and therefore is important to capture in our definition of generalized support.

Extensional constraints (sets of tuples) are interpreted disjunctively, i.e. as long as the set is non-empty, a solution exists. Similarly, support exists if the support set is non-empty. Our generalization of support is to model it as a set of tuples interpreted conjunctively i.e. they all must be valid for support to exist. Thus, a generalized support set is a disjunction of conjunctions ( $\exists \forall$ ); we say support exists if at least one support is present in the set and all the tuples in that support are valid w.r.t. variable domains.

We use the following as a simple running example throughout this section. Example 5.
Consider the constraint $x + y + z ⩾ 2$ with initial signature σ : $x, y, z \in {0, 1}$ . The signature is GAC, and the constraint is satisfied by three tuples: $\begin{array}{l} {[[x + y + z ⩾ 2]]}_{σ} \\ = {⟨ 0, 1, 1 ⟩, ⟨ 1, 0, 1 ⟩, ⟨ 1, 1, 0 ⟩, ⟨ 1, 1, 1 ⟩} \end{array}$

3.1.1. Support properties

A support property is a predicate that takes a set of tuples and a signature, and identifies whether the set of tuples is in fact a support. We will use support properties to define the behaviour of propagators.

Definition 9 (Support property).

Given a schema Y and signature σ over Y, a support property is a predicate $\begin{matrix} P : signature \to 2^{Z^{| Y |}} \to B \end{matrix}$ mapping signatures and sets of integer tuples of length $| Y |$ to a Boolean. We will sometimes write the parameter indicating which signature $P [σ]$ depends on as a subscript $P_{σ}$ or drop it entirely if the property does not depend on a signature.

Definition 10 (Support Set for a property P).

Given a schema Y and a signature σ over Y and a property of sets of Y-tuples, $P_{σ}$ we define the support set for P to be the set: $\begin{array}{l} {support}_{⟨ Y, σ ⟩} (P) \\ \overset{def}{=} {S \subseteq Y - {tuple}_{σ} ∣ P_{σ} (S) \\ \land \forall S^{'} \subset S . \neg P_{σ} (S^{'})} \end{array}$

Note that support sets are minimal w.r.t. the property P since they contain no subset which also satisfies the property.

Consider Example 5, the constraint $x + y + z ⩾ 2$ . One support property is the following $\begin{array}{l} P_{σ} (S) \overset{def}{=} \exists τ \in S . \\ \sum τ ⩾ 2 \land τ [0] = min (σ (x)) \end{array}$ This property admits sets of tuples of any size as long as one tuple satisfies the constraint, and the value for x in that tuple is the minimum value in $σ (x)$ . This support property corresponds to a propagator that prunes the minimum value of x whenever there is no supporting tuple containing it. To enforce GAC, two other properties would be required for y and z. The support set for $P_{σ}$ is ${support}_{⟨ ⟨ x, y, z ⟩, σ ⟩} (P) = {{⟨ 0, 1, 1 ⟩}}$ .

A collection of properties is supported if they all are.

Definition 11 (Support for a collection of properties).

If $P = {P_{1}, \dots, P_{k}}$ is a collection of properties sharing schema Y and σ is a signature over Y, we write $\begin{array}{l} {support}_{⟨ Y, σ ⟩} (P) \\ \overset{def}{=} \forall P \in P . {support}_{⟨ Y, σ ⟩} (P) \neq \emptyset . \end{array}$

3.1.2. Admissible properties and triggers

Our language for properties is unrestrained and allows us to specify properties that are not sensible for specifying propagators. Therefore an admissibility condition is required. We define p-admissibility as follows.

Definition 12 (P-admissibility).

We say a property P is p-admissible if it satisfies the following condition $\begin{array}{l} \forall σ . \forall σ^{'} ⊑ σ . \\ \forall S \subseteq Y - {tuple}_{σ} . \\ (P_{σ} (S) \land S \subseteq Y - {tuple}_{σ^{'}}) \Rightarrow P_{σ^{'}} (S) \end{array}$ In this case, we write $p-admissible (P)$ .

P-admissibility is a kind of stability condition on properties that guarantees that if a $P_{σ} (S)$ holds and the domain is narrowed to $σ^{'}$ , but no tuple is lost from S because of the narrowing, then $P_{σ^{'}} (S)$ must also hold. In the implementation of dynamic-triggered propagators [15], it is implicitly assumed that all supports are p-admissible.

Continuing Example 5, the support property $P_{σ} (S) \overset{def}{=} \exists τ \in S . \sum τ ⩾ 2 \land τ [0] = min (σ (x))$ is p-admissible: $\sum τ ⩾ 2$ does not depend on σ, and $τ [0] = min (σ (x))$ can only be falsified under $σ^{'}$ when the value $min (σ (x))$ is not in $σ^{'} (x)$ . This means τ is not in $⟨ x, y, z ⟩ - {tuple}_{σ^{'}}$ so the implication is trivially satisfied. Suppose $S = {⟨ 0, 1, 1 ⟩}$ . The only way $P_{σ^{'}} (S)$ can be false is if $0 \notin σ^{'} (x)$ . In this case, S contains a tuple that is not valid in $σ^{'}$ therefore the p-admissibility property is trivially true.

A constraint solver has a trigger mechanism which calls propagators when necessary. Each propagator registers an interest in domain events by placing triggers. For example, if a propagator placed a trigger on $⟨ x, a ⟩$ , then the removal of value a in $σ (x)$ would cause the propagator to be called. (This is named a literal trigger [15], or neq event [24].)

In this paper, we focus on literal triggers which can be moved during search. We consider two different types of movable literal trigger: those which are restored as search backtracks (named dynamic literal triggers), and those which are not restored (named watched literals [15]).

The definition of p-admissibility allows the use of dynamic literal triggers, among other types. Watched literals are preferable to dynamic literal triggers because there is no need to restore them when backtracking, which saves space and time. However, it is not always possible to apply watched literals. We define an additional condition on properties named backtrack stability, which is sufficient to allow the use of watched literals.

Definition 13 (Backtrack Stability).

We say a property P is backtrack stable if it satisfies the following condition. $\begin{array}{l} \forall S . \forall σ . \forall σ^{'} ⊑ σ . \\ S \neq \emptyset \Rightarrow \\ P_{σ^{'}} (S) \Rightarrow P_{σ} (S) \end{array}$

Backtrack stability states that any non-empty support S under $σ^{'}$ must remain a support for all signatures σ where σ is larger than $σ^{'}$ . This guarantees that a non-empty support S will remain valid as the search backtracks. The empty support indicates that the property is trivially satisfied; this support is not usually valid after backtracking, so it is excluded here.

Continuing Example 5, the support property $P_{σ} (S) \overset{def}{=} \exists τ \in S . \sum τ ⩾ 2 \land τ [0] = min (σ (x))$ is not backtrack stable because $min (σ (x))$ may not be the same as $min (σ^{'} (x))$ .

Backtrack stability is in fact too strong: it is not necessary for a support to remain valid for all larger signatures, it is only necessary for it to remain valid at signatures that are reachable on backtracking. However it is sufficient for the purposes of this paper.

Backtrack stability also depends on the form of properties. The element support properties presented in Section 4.1.1 are not backtrack stable. However, they can be reformulated to be backtrack stable, by dividing them up as we show in Section 4.1.2.

For some property $P_{σ} (S)$ the support S is evidence that the constraint corresponding to P is consistent. The intuition is that S remains valid evidence until domains are narrowed to the extent that $S ⊈ Y - {tuple}_{σ^{'}}$ (where $σ^{'} ⊑ σ$ ). This is an efficiency measure: a constraint solver can disregard the constraint corresponding to P until $S ⊈ Y - {tuple}_{σ^{'}}$ .

For example, $P_{σ} (S) \overset{def}{=} \forall b \notin σ (j) . ⟨ i, b ⟩ \in S$ is not p-admissible when $j \neq i$ .

Definition 14 (Properties True and False).

We define the constant properties True and False by lifting them to functions of sets of tuples. $\begin{array}{l} True (S) = True \\ False (S) = False \end{array}$

Lemma 8 (True singleton).

For all Y and for every signature σ over Y, $\begin{matrix} {support}_{⟨ Y, σ ⟩} (True) = {\emptyset} \end{matrix}$

Note, that it might be assumed that if any of the domains in σ are empty, then there should be no support, even for the True property. Checking for emptiness is not a function of support, but is done at a higher level.

Lemma 9 (False Empty).

For all Y and for every signature σ over Y, $\begin{matrix} {support}_{⟨ Y, σ ⟩} (False) = \emptyset \end{matrix}$

Corollary 3 (True and False are p-admissible).

The properties True and False are p-admissible.

We can combine supports by taking the conjunctions or disjunctions of their properties.

Definition 15.
We define the conjunction and disjunction of support properties as follows. $\begin{array}{l} {(P \land Q)}_{σ} (S) \overset{def}{=} P_{σ} (S) \land Q_{σ} (S) \\ {(P \lor Q)}_{σ} (S) \overset{def}{=} P_{σ} (S) \lor Q_{σ} (S) \end{array}$

We state the following lemma without proof. Lemma 10 (∧ and ∨ are p-admissible).

Given a schema Y and signature σ for Y and two p-admissible properties P and Q, then $(P \land Q)$ and $(P \lor Q)$ are p-admissible as well.

3.1.3. Extensional support for literals

Definition 16 (Support Property (for a Literal)).

Given a schema Y, a signature σ over Y, and a literal $⟨ i = a ⟩$ , then: $⟨ i = a ⟩$ denotes the property supporting this literal and is given by: $\begin{matrix} ⟨ i = a ⟩ (S) \overset{def}{=} \exists τ \in S . τ [i] = a \end{matrix}$ The support set for $⟨ i = a ⟩$ is simply the set ${support}_{⟨ Y, σ ⟩} (⟨ i = a ⟩)$ .

Corollary 4.
If $S \in {support}_{⟨ Y, σ ⟩} (⟨ i = a ⟩)$ then S is a singleton.
Proof.
Assume $S \in {support}_{⟨ Y, σ ⟩} (⟨ i = a ⟩)$ then $⟨ i = a ⟩ (S)$ holds, i.e. we know $\exists τ \in S . τ [i] = a$ . Thus $| S | ⩾ 1$ . Now, we assume that $| S | > 1$ and show a contradiction. There is at least one tuple in S, such that $τ [i] = a$ . If there is any other tuple $τ^{'} \in S$ where $τ \neq τ^{'}$ then $⟨ i = a ⟩ (S - {τ^{'}})$ holds as well, and since this set is smaller, S was not minimal and so was not a support as we assumed. □
Lemma 11 (Literals are p-admissible).

Given a schema Y and a signature σ on Y, if $i \in {0 \dots | Y | - 1}$ and $a \in σ (Y [i])$ then $⟨ i = a ⟩$ is a p-admissible property.

Proof.
Note that $⟨ i = a ⟩$ does not refer to σ at all and so is p-admissible. □
3.1.4. Generalized support – evidence

Literal support captures support for variable-value pairs. Generalized support is support for some property not necessarily representable by a single tuple. Thus, if any tuple in a generalized support is lost, then the support no longer holds. In Example 4 (GAC AllDifferent) we gave a list of literals as evidence that an AllDifferent constraint is GAC. A list of literals would be represented as a generalized support in our framework by using the support property for a literal (for each literal individually) then finding support for a collection of properties (as in Definition 11).

Constraint solvers typically allow movable triggers to be placed on literals, so the connection between literals and our definition of generalized support is important for this paper. A generalized support may be less compact than the set of literals it represents. However, the implementation of a propagator may correctly place triggers on the set of literals. Generalized support is merely an abstraction used in our framework.

3.2. Soundness and completeness of a collection of propagators

Propagators narrow domains to minimize the search space and provide evidence that the narrowed domains have not eliminated any solutions. Constraints may be implemented by a collection of propagators. To show that the propagators are correct with respect to the constraint they support we show they are sound and complete.

3.2.1. Soundness

Soundness says that for the most restricted non-empty signatures (ones where all domains in the signature have been narrowed to a singleton) the propagator must be able to distinguish between the constraint being empty or inhabited by a single tuple. If support is non-empty at a singleton domain then the constraint must be true there as well. The definition of soundness presented here is related to the one in [26].

Definition 17 (Propagator Soundness).

Given a constraint C with schema Y and a set of properties $P = {P_{1}, \dots, P_{m}}$ we say $P$ is sound with respect to the constraint C if the following holds: $\begin{array}{l} \forall σ . singleton (σ) \Rightarrow \\ ({support}_{⟨ Y, σ ⟩} (P) \Rightarrow {[[C]]}_{σ} \neq \emptyset) \end{array}$

Thinking of support as evidence for truth, one might expect soundness to be characterized as follows: $\begin{matrix} \forall σ . {support}_{⟨ Y, σ ⟩} (P) \Rightarrow {[[C]]}_{σ} \neq \emptyset \end{matrix}$ This is too strong. At a non-singleton signature, support is an approximation to truth. For example, even though a constraint may fail in a particular non-convex domain (i.e. the domain has gaps), a propagator that operates on domain bounds may not recognize the domain is not convex until the signature has been narrowed further.

3.2.2. Completeness

Completeness guarantees that if the extensional representation of a constraint is non-empty at a signature σ then there is support for the family of properties $P$ . The wrinkle on this scheme is that the support may not exist at σ itself, but only at some refined $σ^{'} ⊑ σ$ . If so, we insist that the constraint has not lost any tuples at the refined signature $σ^{'}$ .

Definition 18 (Propagator Completeness).

Given a constraint C with schema Y and a set of properties $P = {P_{1}, \dots, P_{m}}$ we say $P$ is complete with respect to the constraint C if the following holds: $\begin{array}{l} \forall σ . {[[C]]}_{σ} \neq \emptyset \Rightarrow \\ \exists σ^{'} ⊑ σ . \\ {[[C]]}_{σ} \subseteq {[[C]]}_{σ^{'}} \land {support}_{⟨ Y, σ^{'} ⟩} (P) \end{array}$

If $P$ is complete we write $complete (P)$ .

Theorem 1 (Local Completeness).

Given a set of properties $P = {P_{1}, \dots, P_{k}}$ defined over schema Y, if each singleton ${P_{i}}$ is complete then $P$ is complete.

Proof.
If $P$ is supported at σ, then use witness σ for $σ^{'}$ and completeness trivially holds. Suppose there is no support for $P$ at σ where ${[[C]]}_{σ} \neq \emptyset$ . Choose one of the $P_{i} \in P$ such that $\neg {support}_{⟨ Y, σ ⟩} (P_{i})$ and let $σ^{'}, σ^{'} ⊏ σ$ be the signature claimed to exist in the proof of completeness of $P_{i}$ . By completeness of ${P_{i}}$ , ${[[C]]}_{σ} \subseteq {[[C]]}_{σ^{'}}$ . If there is support for $P$ at $σ^{'}$ then $P$ is complete. If not, iterate this process by choosing another $P_{k} \in P$ that is not supported at $σ^{'}$ . The fixed-point of this process must yield a signature $\hat{σ}$ such that ${support}_{⟨ X, \hat{σ} ⟩} (P)$ . The fixed-point exists because ⊏ is a well-founded relation on signatures. □

Our definition of completeness ensures that a propagator derived from a support property does not fail early, therefore it is merely a correctness property. It is similar in intention to Maher’s definition of weak completeness [20], although Maher’s definition only applies to singleton domains.

Soundness and completeness as defined here are the minimum conditions required for a propagator to operate correctly, thus popular notions of consistency such as GAC, $bound (Z)$ and $bound (R)$ are sound and complete, and therefore are supported in our framework. Soundness and completeness are satisfied by very simple support properties such as: $\begin{array}{rcl} P_{σ} (S) & \overset{def}{=} & (\neg singleton (σ) \to S \neq \emptyset) \\ \land (singleton (σ) \to {[[C]]}_{σ} \neq \emptyset) \end{array}$

This property corresponds to a propagator that waits until all variables are assigned before checking the constraint. Any practical propagator is stronger than this.

Soundness and completeness are not the only options for characterizing the correctness of a set of generalized support properties. For example, in [15] it is shown that a set of properties imply the domain is GAC. Other forms of consistency such as bound consistency could also serve as correctness conditions for a set of properties.
3.3. Formal development of constraint propagators

The methodology for formal development of propagators for a constraint C is as follows:

Describe a set of support properties ( $P = {P_{1}, \dots, P_{k}}$ ) that characterize constraint C and prove that they are p-admissible.

For each property $P_{i}$ , give a constructive proof of the propagation schema given in Definition 19. The computational content of these proofs gives a correct-by-construction algorithm for each propagator.

Prove the soundness and completeness of $P$ with respect to C. This shows the collection of propagators are correct w.r.t. the constraint C. This proof often reuses the propagation schema proofs.

3.3.1. The propagation schema

We present the following schematic formula whose constructive proofs capture the methods of generating support for a particular property P.

Definition 19 (Propagation Schema).

Given a signature σ, a schema X, and a p-admissible property P, constructive proofs of the following statement yield a propagator for P. $\begin{array}{l} \forall S \in {support}_{⟨ X, σ ⟩} (P) . \\ \forall σ_{1} ⊑ σ . nonempty (σ_{1}) \Rightarrow \\ S \notin {support}_{⟨ X, σ_{1} ⟩} (P) \Rightarrow \\ findNewSupport (X, P, σ_{1}) \\ \lor noNewSupport (X, P, σ_{1}) \end{array}$ When an existing support S has been lost in a signature $σ_{1} ⊑ σ$ , a new support and a new signature $σ_{2} ⊑ σ_{1}$ are found in findNewSupport. Otherwise, noNewSupport states that there is no new support to be found. $\begin{array}{l} findNewSupport (X, P, σ_{1}) \\ \overset{def}{=} (\exists σ_{2} ⊑ σ_{1} . nonempty (σ_{2}) \\ \land \exists S^{'} \in {support}_{⟨ X, σ_{2} ⟩} (P) . \\ \forall σ_{3} . σ_{2} ⊏ σ_{3} ⊑ σ_{1} \Rightarrow \\ {support}_{⟨ X, σ_{3} ⟩} (P) = \emptyset) \\ noNewSupport (X, P, σ_{1}) \\ \overset{def}{=} \forall σ_{2} ⊑ σ_{1} . nonempty (σ_{2}) \Rightarrow \\ {support}_{⟨ X, σ_{2} ⟩} (P) = \emptyset \end{array}$

We are interested in constructive proofs2

²
There is a classical proof of propagator schema that is independent of the property P and carries no interesting computational content.

of the propagator schema when P is instantatied to individual support properties.

Given a p-admissible support property P, a constructive proof of the propagator schema yields a function that takes as input a set S, evidence that $S \in {support}_{⟨ X, σ ⟩} (X)$ , a signature $σ_{1}$ and evidence that $σ_{1} ⊑ σ$ , evidence that $S \notin {support}_{⟨ X, σ_{1} ⟩} (P)$ and returns one of two items:

a new signature $σ_{2}$ , together with evidence that $σ_{2} ⊑ σ_{1}$ , a set of tuples $S^{'}$ and evidence that $S^{'} \in {support}_{⟨ X, σ_{2} ⟩} (P)$ and evidence that $σ_{2}$ is maximal.

Evidence that there is no support for P in $σ_{1}$ or for any smaller signature.

Lemma 12 (Non-empty in propagation schema).

In the propagation schema, if we assume the antecedent $S \notin {support}_{⟨ X, σ_{1} ⟩} (P)$ for $σ_{1} ⊑ σ$ then $S \neq \emptyset$ .

Proof.
Because property P is p-admissible, if we have $\emptyset \in {support}_{⟨ X, σ ⟩} (P)$ then $\forall σ_{1} ⊑ σ . \emptyset \in {support}_{⟨ X, σ_{1} ⟩} (P)$ . □

4. Generating propagators

In this section we present three case studies of applying our methodology.

4.1. A propagator for the element constraint

The element constraint is widely useful in specifying a large class of constraint problems. It has the form $element (X, y, z)$ where X is a vector of variables and y and z are variables. The meaning of the element constraint is the set of all coherent tuples on the schema $⟨ X \cdot y \cdot z ⟩$ of the following form. $\begin{matrix} τ = ⟨ v_{1}, \dots, v_{i - 1}, j, v_{i + 1}, \dots, v_{k}, i, j ⟩ \end{matrix}$ Thus, $τ [k + 1] = i$ indexes $⟨ v_{1}, \dots, v_{k} ⟩$ and $τ [k + 2] = τ [i]$ .

Definition 20 (Element Semantics).

$\begin{array}{l} {[[element (X, y, z)]]}_{σ} = ⟨ ⟨ X \cdot y \cdot z ⟩, R ⟩ \\ where \\ R = {τ \in ⟨ X \cdot y \cdot z ⟩ - {tuple}_{σ} ∣ \\ k = | X | \land τ [k + 1] \in {1 \dots k} \\ \land τ [k + 2] = τ [τ [k + 1]]} \end{array}$

The element constraint is widely used because it represents the very basic operation of indexing a vector [28]. For example, Gent et al. model Langford’s number problem and quasigroup table generation problems using element [15].

In [15, pp. 188] three properties to establish GAC for the element constraint are characterized. We restate theorem 1 from that paper here:

Theorem 2 (Theorem 1 of reference [15]).

Given a constraint of the form $Element (X, y, z)$ , domains given by a signature σ are Generalized Arc Consistent if and only if all of the following hold. $\begin{array}{l} (1) & \forall i \in σ (y) . σ (y) = {i} \Rightarrow σ (X [i]) \subseteq σ (z) \\ (2) & \forall i \in σ (y) . σ (X [i]) \cap σ (z) \neq \emptyset \\ (3) & σ (z) \subseteq ⋃_{i \in σ (y)} σ (X [i]) \end{array}$

4.1.1. Support properties

Each of the three properties above can be characterized as support properties.

Definition 21 (Element Support Properties).

With a schema X and variables y and z and a signature σ, there are three properties corresponding to three propagators for establishing GAC for the element constraint $Element (X, y, z)$ . Let k be $| X |$ , then $k + 1$ is the index of y and $k + 2$ is the index of z in the schema $(X \cdot y \cdot z)$ . $\begin{array}{l} P_{1} [σ] (S) \\ \overset{def}{=} (\exists i, j \in σ (y) . \\ i \neq j \land ⟨ k + 1, i ⟩ \in S \land ⟨ k + 1, j ⟩ \in S) \\ \lor \forall i \in σ (y) . \forall a \in σ (X [i]) . ⟨ k + 2, a ⟩ \in S \\ P_{2} [σ] (S) \overset{def}{=} \forall i \in σ (y) . \exists a \in σ (z) . \\ ⟨ i, a ⟩ \in S \land ⟨ k + 2, a ⟩ \in S \\ P_{3} [σ] (S) \overset{def}{=} \forall a \in σ (z) . \exists i \in σ (y) . \\ ⟨ i, a ⟩ \in S \land ⟨ k + 1, i ⟩ \in S \end{array}$

Note that for property $P_{1}$ , the first disjunct is true iff the domain of the index variable y has more than one element, $| σ (y) | > 1$ . Support for this disjunct is a pair of literals $⟨ k + 1, i ⟩$ and $⟨ k + 1, j ⟩$ where $i, j \in σ (y), i \neq j$ .3

³
This specification corresponds to a set of dynamic literal triggers [15]. Ideally a static assignment trigger would be used for $P_{1}$ , which would trigger the propagator when y is assigned. However, assignment triggers are outside the scope of this paper.

Logically,

(\exists i, j \in σ (y) . i \neq j)

is equivalent, but for our purposes we must provide p-admissible support. Once the domain of the index variable is a singleton (

σ (y) = {i}

), the second disjunct of

P_{1}

may be satisfied. This disjunct is supported by a set of

| σ (X [i]) |

literals of the form

⟨ k + 2, a ⟩

, one literal for each

a \in σ (X [i])

. This is evidence for

σ (X [i]) \subseteq σ (z)

since

k + 2

is the index of z in the schema

(X \cdot y \cdot z)

Property $P_{2}$ is supported iff $σ (X [i]) \cap σ (z)$ is non-empty for every $i \in σ (y)$ . The support is $2 m$ literals where $m = | σ (y) |$ , two for each $i \in σ (y)$ . These have the form $⟨ i, a ⟩$ and $⟨ k + 2, a ⟩$ where a is some value in $σ (z)$ . If there is no support, then $σ (X [i]) \cap σ (z) = \emptyset$ .

Property $P_{3}$ is supported iff $\begin{matrix} σ (z) \subseteq ⋃_{i \in σ (y)} σ (X [i]) . \end{matrix}$ The support is a set of $2 m$ literals where $m = | σ (z) |$ , two for each $a \in σ (z)$ . The literals have the form $⟨ i, a ⟩$ and $⟨ k + 1, i ⟩$ where i is some value in $σ (y)$ . If there is no support then for some $a \in σ (z)$ , for all i $a \notin σ (X [i])$ .

It is easy to prove that the three properties act as intended: Theorem 3.

Given a signature σ, we have:

(1) is true if and only if $\exists S . P_{1} [σ] (S)$

(2) is true if and only if $\exists S . P_{2} [σ] (S)$

(3) is true if and only if $\exists S . P_{3} [σ] (S)$

Proof.

The if directions are all easy. For (1), if the first disjunct of $P_{1}$ is satisfied then $| σ (y) | > 1$ so (1) is vacuous. If the second disjunct is satisfied, it ensures that $σ (X [i]) \subseteq σ (z)$ . If $P_{2} (S)$ is true then, for each element of the domain of the index variable y, there is a value $a \in σ (X [i]) \cap σ (z)$ , establishing (2). If $P_{3} (S)$ is true then, for any value a in $σ (z)$ there is a value i of the index variable with $a \in σ (X [i])$ , proving that (3) holds.

For Only if, first suppose that (1) is true. If $| σ (y) | > 1$ then we can find $i, j$ to satisfy the first disjunct of $P_{1}$ , and set $S = {⟨ k + 1, i ⟩, ⟨ k + 1, j ⟩}$ . Otherwise, we have $σ (y) = {i}$ and $σ (X [i]) \subseteq σ (z)$ . We can thus set $S = {⟨ k + 2, a ⟩ ∣ a \in σ (X [i])}$ .

Suppose (2) is true. We have $σ (X [i]) \cap σ (z) \neq \emptyset$ for each $i \in σ (y)$ . So for each i there is thus some $a_{i}$ with $a_{i} \in σ (X [i]) \cap σ (z)$ . We can thus set $S = {⟨ i, a_{i} ⟩, ⟨ k + 2, a_{i} ⟩ ∣ i \in σ (y)}$ .

Suppose (3) is true. Since $σ (z) \subseteq ⋃_{i \in σ (y)} σ (X [i])$ , we have for each $a \in σ (z)$ some $i_{a}$ such that $i_{a} \in σ (y)$ and $a \in σ (X [i_{a}])$ . We can thus set $S = {⟨ i_{a}, a ⟩, ⟨ k + 1, i_{a} ⟩ ∣ a \in σ (z)}$ . □

4.1.2. P-admissibility and backtrack stability

Following our methodology, we first prove that properties $P_{1}$ , $P_{2}$ and $P_{3}$ are p-admissible.

Lemma 13 ( $P_{1}$ is p-admissible).

$\begin{matrix} p - admissible (P_{1}) \end{matrix}$

Proof.
We case split on the disjuncts of $P_{1}$ . The first disjunct requires distinct values $i, j \in σ (y)$ . Assuming $S \subseteq ⟨ X \cdot y \cdot z ⟩ - {tuple}_{σ^{'}}$ , $i, j \in σ^{'} (y)$ because the two necessary literals are in S, therefore $P_{1} [σ^{'}] (S)$ holds.

For the second disjunct of $P_{1}$ , since $σ^{'} ⊑ σ$ we can see that $σ^{'} (y) \subseteq σ (y)$ and $\forall i . σ^{'} (X [i]) \subseteq σ (X [i])$ , therefore all necessary literals are present in S and $P_{1} [σ^{'}] (S)$ holds. □
Lemma 14 ( $P_{2}$ is p-admissible).

$\begin{matrix} p - admissible (P_{2}) \end{matrix}$

Proof.
Since $σ^{'} ⊑ σ$ , $σ^{'} (y) \subseteq σ (y)$ therefore there are fewer (or the same) values of i to consider under $σ^{'}$ . Assuming $S \subseteq ⟨ X \cdot y \cdot z ⟩ - {tuple}_{σ^{'}}$ , for each i, $⟨ k + 2, a ⟩ \in S$ therefore $a \in σ^{'} (z)$ and $P_{2} [σ^{'}] (S)$ holds. □
Lemma 15 ( $P_{3}$ is p-admissible).

$\begin{matrix} p - admissible (P_{3}) \end{matrix}$

Proof.
The proof is the same as above, with z and y exchanged, i and a exchanged, and $k + 1$ substituted for $k + 2$ . □

$P_{1}$ , $P_{2}$ and $P_{3}$ are not backtrack stable according to Definition 13. However, $P_{2}$ and $P_{3}$ can be straightforwardly reformulated to be backtrack stable: the universal quantifier is expanded to a conjunction using the initial signature, then each conjunct is made into an individual property, subscripted by i or a respectively. For example, $P_{2}$ is transformed as follows. $\begin{array}{l} P_{2, i} [σ] (S) \overset{def}{=} i \in σ (y) \Rightarrow \\ (\exists a \in σ (z) . ⟨ i, a ⟩ \in S \land ⟨ k + 2, a ⟩ \in S) \end{array}$

Each of these smaller properties then requires two literals as support, or (if $i \notin σ (y)$ ) the empty set, and they are backtrack stable. $P_{1}$ can be reformulated to be backtrack stable, by expanding out the universal quantifiers in the same way as for $P_{2}$ . $P_{1}$ would be subscripted by i and a, $\forall i \in σ (y)$ replaced with $i \in σ (y) \Rightarrow$ , and the same for $\forall a \in σ (X [i])$ . These reformulations give a large set of properties, so for the sake of simplicity we use the original $P_{1}$ , $P_{2}$ and $P_{3}$ .
4.1.3. Proofs of the propagation schema

Now that we have established p-admissibility for each of $P_{1}$ , $P_{2}$ and $P_{3}$ we prove the instances of the propagator schema for each of them.

Theorem 4 ( $P_{1}$ Support Generation).

We consider $P_{1}$ on constraint $Element (X, y, z)$ . We claim that Definition 19 (propagation schema) holds for $P_{1}$ .

Proof.
Let C be an element constraint of the form $Element (X, y, z)$ where $| X | = k$ and let σ and $σ_{1}$ be signatures mapping the variables in $X . y . z$ to their respective domains. We claim the following: $\begin{array}{l} \forall S \in {support}_{⟨ X . y . z, σ ⟩} (P) . \\ \forall σ_{1} ⊑ σ . nonempty (σ_{1}) \Rightarrow \\ S \notin {support}_{⟨ X . y . z, σ_{1} ⟩} (P) \Rightarrow \\ findNewSupport (X . y . z, P, σ_{1}) \\ \lor noNewSupport (X . y . z, P, σ_{1}) \\ findNewSupport (X . y . z, P, σ_{1}) \\ \overset{def}{=} (\exists σ_{2} ⊑ σ_{1} . nonempty (σ_{2}) \\ \land \exists S^{'} \in {support}_{⟨ X . y . z, σ_{2} ⟩} (P) . \\ \forall σ_{3} . σ_{2} ⊏ σ_{3} ⊑ σ_{1} \Rightarrow \\ {support}_{⟨ X . y . z, σ_{3} ⟩} (P) = \emptyset) \\ noNewSupport (X . y . z, P, σ_{1}) \\ \overset{def}{=} \forall σ_{2} ⊑ σ_{1} . nonempty (σ_{2}) \Rightarrow \\ {support}_{⟨ X . y . z, σ_{2} ⟩} (P) = \emptyset \end{array}$

The proof consists of constructing $σ_{2}$ and $S^{'}$ for all cases, given $σ_{1}$ . When $σ_{2} ⊏ σ_{1}$ , we also prove that $σ_{2}$ is maximal (i.e. there exists no $σ_{3}$ ). $\begin{array}{l} | σ_{1} (y) | > 1 \Rightarrow \\ S^{'} = {⟨ k + 1, min (σ_{1} (y)) ⟩, \\ ⟨ k + 1, max (σ_{1} (y)) ⟩} \\ \land σ_{2} = σ_{1} \\ σ_{1} (y) = {i} \Rightarrow \\ σ_{2} (X [i]) = σ_{1} (z) \cap σ_{1} (X [i]) \\ \land (\forall x \in ⟨ X \cdot y \cdot z ⟩ . x \neq X [i] \Rightarrow \\ σ_{2} (x) = σ_{1} (x)) \\ \land S^{'} = ⋃_{b \in σ_{2} (X [i])} {⟨ k + 2, b ⟩} \end{array}$ For the second case above, it remains to be shown that $σ_{2}$ is nonempty and maximal. We prove that $σ_{2}$ is maximal. For all values $b \in σ_{2} (X [i])$ , a supporting literal $⟨ z, b ⟩$ is required in $S^{'}$ . Therefore, $P_{1}$ implies that $σ_{2} (X [i]) \subseteq σ_{2} (z)$ , hence $σ_{2} (X [i]) = σ_{1} (z) \cap σ_{1} (X [i])$ is maximal. For all other variables w, $σ_{2} (w) = σ_{1} (w)$ , therefore $σ_{2}$ is maximal under ⊑.

If $σ_{2} (X [i]) = \emptyset$ (i.e. $σ_{1} (z) \cap σ_{1} (X [i]) = \emptyset$ ), $σ_{2}$ is empty. Since $σ_{2}$ is the maximal one which satisfies $P_{1}$ , the second disjunct (noNewSupport) of the consequent of the schema holds. □
Theorem 5 ( $P_{2}$ Support Generation).

We consider $P_{2}$ on constraint $Element (X, y, z)$ . We claim that Definition 19 (propagation schema) holds for $P_{2}$ .

Proof.
Let $k = | X |$ , and $σ_{1}$ and $σ_{2}$ be signatures mapping the variables in $X . y . z$ to their respective domains. The proof is by constructing $σ_{2}$ and $S^{'}$ to satisfy the first disjunct of the consequent of the schema. $\begin{array}{l} σ_{2} (y) = {i \in σ_{1} (y) ∣ \exists a \in σ_{1} (z) . a \in σ_{1} (X [i])} \\ \forall x \in ⟨ X . z ⟩ σ_{2} (x) = σ_{1} (x) \\ S^{'} = ⋃_{i \in σ_{2} (y)} {⟨ i, a ⟩, ⟨ k + 2, a ⟩} \end{array}$ $σ_{2}$ is maximal: the constructed $σ_{2}$ is identical to $σ_{1}$ except for the set $σ_{2} (y)$ . For each value i of $σ_{2} (y)$ , $P_{2}$ requires that there exists a value a in the domains of $X [i]$ and z. $σ_{2} (y)$ is the maximal subset of $σ_{1} (y)$ which satisfies this condition, therefore $σ_{2}$ is maximal under ⊑.

If $σ_{2}$ is empty, then (since $σ_{2}$ is maximal) the second disjunct of the consequent of the schema holds. □
Theorem 6 ( $P_{3}$ Support Generation).

We consider $P_{3}$ on constraint $Element (X, y, z)$ . We claim that Definition 19 (propagation schema) holds for $P_{3}$ .

Proof.
Let $k = | X |$ , and $σ_{1}$ and $σ_{2}$ be signatures mapping the variables in $X . y . z$ to their respective domains. The proof is by constructing $σ_{2}$ and $S^{'}$ to satisfy the first disjunct of the consequent of the schema. $\begin{array}{l} σ_{2} (z) = {a \in σ_{1} (z) ∣ \exists i \in σ_{1} (y) . a \in σ_{1} (X [i])} \\ \forall x \in X . y . σ_{2} (x) = σ_{1} (x) \\ S^{'} = ⋃_{a \in σ_{2} (z)} {⟨ i, a ⟩, ⟨ k + 1, i ⟩} \end{array}$ The constructed $σ_{2}$ is identical to $σ_{1}$ except for the set $σ_{2} (z)$ . For each value a of $σ_{2} (z)$ , $P_{3}$ requires that there exists an index i such that $a \in σ_{2} (X [i])$ and $i \in σ_{2} (y)$ . $σ_{2} (z)$ is the maximal subset of $σ_{1} (y)$ which satisfies this condition, therefore $σ_{2}$ is maximal under ⊑.

If $σ_{2}$ is empty, then (since $σ_{2}$ is maximal) the second disjunct of the consequent of the schema holds. □

4.1.4. Soundness and completeness

Now we prove that the conjunction of the element support properties (Definition 21) is sound and complete using the semantics of element (Definition 20). We will write $P_{e}$ for the set ${P_{1}, P_{2}, P_{3}}$ .

Lemma 16 ( $P_{e}$ is sound).

$\begin{array}{l} \forall σ . singleton (σ) \Rightarrow \\ ({support}_{⟨ X . y . z, σ ⟩} (P_{e}) \Rightarrow \\ {[[element (X, y, z)]]}_{σ} \neq \emptyset) \end{array}$

Proof.
Let σ be an arbitrary singleton signature. Since σ is a singleton it encodes a single tuple (say τ). Assume ${support}_{⟨ X . y . z, σ ⟩} (P_{e})$ holds. That is, supports for $P_{1} [σ]$ , $P_{2} [σ]$ and $P_{3} [σ]$ are non empty. Now, consider $P_{1}$ . Since $| σ (y) | = 1$ we know the first disjunct can not hold and so we must have support for the second. Since $σ (y) \neq \emptyset$ we know that there is a single tuple supporting the second disjunct of $P_{1}$ and since $| σ (X [i]) | = 1$ , to support $P_{1}$ , τ must have the form $⟨ x_{1}, \dots, x_{i - 1}, a, x_{i + 1}, \dots, x_{k}, i, a ⟩$ . This same tuple supports $P_{2}$ and $P_{3}$ . This tuple is clearly in ${[[element (X, y, z)]]}_{σ}$ and so soundness holds. □
Theorem 7 ( ${P_{1}}$ complete).

$\begin{array}{l} \forall σ . {[[element (X, y, z)]]}_{σ} \neq \emptyset \Rightarrow \\ \exists σ^{'} ⊑ σ . \\ {[[element (X, y, z)]]}_{σ^{'}} \\ = {[[element (X, y, z)]]}_{σ} \\ \land {support}_{⟨ X . y . z, σ^{'} ⟩} ({P_{1}}) \end{array}$

Proof.
Assume ${[[element (X, y, z)]]}_{σ} \neq \emptyset$ for arbitrary σ. If ${support}_{⟨ X, y, z, σ ⟩} (P_{1}) \neq \emptyset$ then the theorem is trivially true, so we assume that ${support}_{⟨ X . y . z, σ ⟩} (P_{1}) = \emptyset$ and construct a signature $σ^{'}$ that does not eliminate any solutions from the constraint and in which $P_{1}$ has support.

The first disjunct of $P_{1}$ is supported whenever $| σ (y) | > 1$ and so if $P_{1}$ is not supported $σ (y) = {i}$ or $σ (y) = \emptyset$ ; by assumption no domain of σ is empty and so $σ (y) = {i}$ . To falsify the second disjunct of $P_{1}$ when $σ (y) = {i}$ , there must be some $a \in σ (X [i])$ such that the literal $⟨ k + 2, a ⟩$ can not be supported. This happens for any $a \in σ (X [i])$ where $a \notin σ (z)$ . Let $σ_{1}$ be a signature that is just like σ except that $\begin{matrix} σ_{1} (z) = σ (z) \cap σ (X [i]) \end{matrix}$ Since the constraint is non-empty the intersection is non-empty. The second disjunct of $P_{1}$ supports this new signature so it supports $P_{1}$ . Clearly $σ_{1} ⊑ σ$ and so it only remains to show that the meaning of the constraint does not change under the new signature. It is enough to show that $\begin{array}{l} {[[element (X, y, z)]]}_{σ} \\ \subseteq {[[element (X, y, z)]]}_{σ_{1}} \end{array}$ Assume $τ \in {[[element (X, y, z)]]}_{σ}$ . Then $τ \in ⟨ X \cdot y \cdot z ⟩ - {tuple}_{σ}$ is coherent and is of the form $\begin{matrix} τ = ⟨ x_{1}, \dots, x_{i - 1}, a, x_{i + 1}, \dots, x_{k}, i, a ⟩ \end{matrix}$ Since τ is an $⟨ X \cdot y \cdot z ⟩ - {tuple}_{σ}$ , we know $τ [j] \in σ (X [j])$ for all $j \in {1 \dots k + 2}$ . To construct $σ_{1}$ we simply eliminated elements $b \in σ (z)$ such that $b \notin σ (X [i])$ so since $a \in σ (X [i])$ , $a \in σ_{1} (X [i])$ and $a \in σ_{1} (z)$ and so $τ \in {[[element (X, y, z)]]}_{σ_{1}}$ . □
Theorem 8 ( ${P_{2}}$ complete).

Proof.
Note that if $P_{2} [σ]$ is unsupported then $σ (X [i]) \cap σ (z) = \emptyset$ . But since we assume that ${[[element (X, y, z)]]}_{σ} \neq \emptyset$ , this is impossible and so $P_{2} [σ]$ must be supported and completeness trivially holds. □
Theorem 9
( ${P_{3}}$ complete).
Proof.
If there is no support for $P_{3} [σ]$ then $\begin{matrix} \exists a \in σ (z) . \forall i \in σ (y) . a \notin σ (X [i]) \end{matrix}$ Just let $σ^{'}$ be the same as σ except that we remove all such elements from the domain of z in $σ^{'}$ . $\begin{matrix} σ^{'} (z) = σ (z) \cap ⋃_{i \in σ (y)} σ (X [i]) \end{matrix}$ Clearly $σ^{'} (z) \subset σ (z)$ . The elements that have been removed could not be included in a solution of ${[[element (X, y, z)]]}_{σ}$ and so we have lost no answers. Thus, we have shown $P_{3}$ is complete. □
Corollary 5
( $P_{e}$ is complete).
Proof.
The completeness of $P_{e}$ follows from local completeness (Theorem 1) and the completeness of $P_{1}$ , $P_{2}$ and $P_{3}$ . □

4.1.5. Discussion

The propagators derived here to enforce GAC on the element constraint are not identical to those presented by Gent et al. [15]. However they do follow the same general scheme. The main difference is that the propagators here use dynamic literal triggers in place of watched literals and a static assignment trigger. The concept of generalized support has allowed us to create these propagators within one formal framework.

4.2. Triggering the AllDifferent constraint

The AllDifferent constraint is widely used and has a powerful GAC propagator introduced by Régin [22]. In this section we give a sketch of how the propagator may be represented in our framework. The propagator is based on graph theory. It establishes GAC in a single invocation, but can be expensive. AllDifferent ensures that each variable in the schema takes a different value, as defined below.

Definition 22 (AllDifferent Semantics).

$\begin{array}{l} {[[AllDiff (X)]]}_{σ} = ⟨ X, R ⟩ \\ where \\ R = {τ \in X - {tuple}_{σ} ∣ \\ \forall i, j \in {0 \dots | X | - 1} . i \neq j \to \\ τ [i] \neq τ [j]} \end{array}$

Gent, Miguel and Nightingale [16] presented a method for using dynamic literal triggers with Régin’s algorithm. The key idea is to construct a set of literal supports such that (while all the literal supports are valid) the algorithm will always follow the same trajectory and therefore no new value deletions are necessary to maintain GAC.

Given that the algorithm enforces GAC in a single call, it is most appropriate to represent it with a single support property. The support property is very simple and essentially treats the propagator as a black box. Our goal is to capture the interaction between the propagator and the rest of the solver, not to represent the entire propagator as we did for the Element constraint.

Definition 23 (AllDifferent Support Property).

Given a schema X and a signature σ over X, we define a support property for the constraint $C = AllDiff (X)$ . $GAC (σ)$ is true iff σ is a GAC signature w.r.t. $C$ . Let $Prop (σ)$ be the set of literal supports defined by Gent et al. [16, Section 5.2]. $\begin{array}{l} P [σ] (S) \\ \overset{def}{=} GAC (σ) \\ \land \forall ⟨ i, a ⟩ \in Prop (σ) . ⟨ i, a ⟩ \in S \end{array}$

In Example 4 we gave an example of $Prop (σ)$ for a small AllDifferent with three variables. $Prop (σ)$ contained at least two literals of each variable. In fact, $Prop (σ)$ always contains at least two literals of every variable that has more than one value in σ. Therefore all supports S will contain more than one tuple (except in the case where all variables are assigned).

4.2.1. P-admissibility

We make an informal argument that $P [σ] (S)$ is p-admissible. For the most part this is done by referring to proofs in Gent et al. [16]. To establish p-admissibility of $P [σ] (S)$ , we need to ensure that for all $σ^{'} ⊑ σ$ where S is still valid (i.e. $S \in X - {tuple}_{σ^{'}}$ ), the two parts of the support property remain true: the smaller signature $σ^{'}$ is GAC; and S contains the set of literals returned by $Prop (σ^{'})$ .

Gent et al. prove that the algorithm will make no value deletions under $σ^{'}$ [16, Section 5.2] since $σ^{'}$ contains all the literals in $Prop (σ)$ . Therefore $σ^{'}$ must be GAC by correctness of the algorithm. This gives us the first part of the support property: $GAC (σ^{'})$ . As part of the proof, it is shown that a DFS procedure on a digraph can perform the exact same search under $σ^{'}$ as it does under σ. Here we assume that the DFS does perform the same search (which can be achieved by fixing the order of the vertices). The sets of literals $Prop (σ)$ and $Prop (σ^{'})$ are produced directly by the DFS, and (under our assumption) will be equal. Therefore the second part of the stability property is true.

4.2.2. Propagation schema, soundness and completeness

We sketch a proof of the propagation schema for $P [σ] (S)$ . Given an existing support S under signature σ, and a smaller signature $σ_{1} ⊑ σ$ where S is no longer a support, the propagation schema has two cases: construction of the largest possible $σ_{2} ⊑ σ_{1}$ where $σ_{2}$ is GAC, and creation of a new support $S^{'}$ ; or failure when GAC would empty the variable domains. By correctness of the GAC propagator for AllDifferent [22] and correctness of the dynamic literal triggers [16], the GAC propagator may be used as a constructive proof of the propagation schema.

Ordinarily we would prove soundness and completeness of a collection of properties. However, since we have a single property that precisely enforces GAC, these proofs are not necessary because both soundness and completeness are consequences of GAC.

4.2.3. Discussion

We have shown that our framework is sufficiently general to capture the triggering of the GAC AllDifferent propagator. GAC AllDifferent differs substantially from Element, yet our framework can represent both.

4.3. New watched literal propagators for occurrence constraints

The two constraints $occurrenceleq (X, a, c)$ and $occurrencegeq (X, a, c)$ (very similar to atmost and atleast) restrict the number of occurrences of a value in a vector of variables. If $occ (X, a)$ is the occurrences of value a in X, occurrenceleq states that $occ (X, a) ⩽ c$ and occurrencegeq states that $occ (X, a) ⩾ c$ .

Occurrence constraints arise in many problems. For example, in a round-robin tournament schedule, it may be required that no team plays more than twice at each stadium [29], represented by occurrenceleq constraints. In car sequencing (car factory scheduling), occurrence constraints may be used to avoid placing too much demand on a work-station [25].

First we present the formal semantics of occurrenceleq and occurrencegeq, followed by support properties for the two constraints.

Definition 24 (Occurrenceleq Semantics).

$\begin{array}{l} {[[occurrenceleq (X, a, c)]]}_{σ} = ⟨ X, R_{X} ⟩ \\ where R_{X} = {τ \in X - {tuple}_{σ} ∣ \\ | {i ∣ τ [i] = a} | ⩽ c} \end{array}$

Definition 25 (Occurrencegeq Semantics).

$\begin{array}{l} {[[occurrencegeq (X, a, c)]]}_{σ} = ⟨ X, R_{X} ⟩ \\ where R_{X} = {τ \in X - {tuple}_{σ} ∣ \\ | {i ∣ τ [i] = a} | ⩾ c} \end{array}$

4.3.1. Support properties

Definition 26 (Occurrence Support Properties).

Given a schema X, value a and occurrence count c, $P_{l}$ is the support property for the occurrenceleq constraint, and similarly $P_{g}$ is the property for occurrencegeq. $\begin{array}{rcl} P_{l} [σ] (S) & \overset{def}{=} & (\exists I \subseteq {1 \dots | X |} . \\ | I | = (| X | - c + 1) \\ \land \forall i \in I . \exists b \neq a . ⟨ i, b ⟩ \in S) \\ \lor \\ (\exists I \subseteq {1 \dots | X |} . \\ | I | = (| X | - c) \\ \land \forall i \in I . a \notin σ (X [i])) \\ P_{g} [σ] (S) & \overset{def}{=} & (\exists I \subseteq {1 \dots | X |} . \\ | I | = (c + 1) \\ \land \forall i \in I . ⟨ i, a ⟩ \in S) \\ \lor \\ (\exists I \subseteq {1 \dots | X |} . \\ | I | = c \\ \land \forall i \in I . ∄ b \in σ (X [i]) . b \neq a) \end{array}$

$P_{g}$ is slightly simpler, so we consider it first. There are two forms of support which can satisfy $P_{g}$ , corresponding to the two disjuncts. The first disjunct can be satisfied if $c + 1$ variables have a in their domain, by a support set which contains $c + 1$ literals mapping distinct variables to a. The second disjunct is satisfied if c variables are set to a. In this case, S may be empty.

When it is no longer possible to satisfy the first disjunct, a corresponding propagator must narrow the domains to satisfy the second disjunct, by setting c variables to a. At this point, the constraint is trivially satisfied so S may be empty.

$P_{l}$ is very similar, and essentially works in the same way except that it requires $| X | - c$ non-occurrences of a rather than c occurrences of a.

4.3.2. P-admissibility and backtrack stability

We now prove that both properties meet the p-admissibility requirement.

Theorem 10 ( $P_{l}$ is p-admissible).

The property $P_{l}$ is p-admissible according to Definition 12 .

Proof.
We case split on the disjuncts of $P_{l}$ . The first disjunct does not refer to $σ^{'}$ , and (since S has not changed) it remains true. The second disjunct is satisfied by $S = \emptyset$ only when the constraint is a tautology. Since $a \notin σ (X [i])$ and $σ^{'} ⊑ σ$ , then $a \notin σ^{'} (X [i])$ and the property remains true. □
Theorem 11 ( $P_{g}$ is p-admissible).

The property $P_{g}$ is p-admissible according to Definition 12 .

Proof.
We case split on the disjuncts of $P_{g}$ . The first disjunct does not refer to $σ^{'}$ , and (since S has not changed) it remains true. The second disjunct is satisfied by $S = \emptyset$ only when the constraint is a tautology. Since $σ (X [i]) \subseteq {a}$ and $σ^{'} ⊑ σ$ , then $σ^{'} (X [i]) \subseteq {a}$ and the property remains true. □

In order for the two propagators to make use of watched literals, we must prove that both properties are backtrack stable. The watched literals representing a support are not backtracked, so a support must remain a support as search backtracks (and the domains are widened). Theorem 12 (Occurrence Backtrack Stable).

The two occurrence support properties are backtrack stable according to Definition 13 .

Proof.
For both properties, the second disjunct is irrelevant because it is satisfied by $S = \emptyset$ only when the constraint is a tautology. The support ∅ is not required to be backtrack stable. In both properties the first disjunct requires a fixed number ( $| X | - c + 1$ or $c + 1$ ) of literals to be in S (with variable indices I). It is clear that for any $σ^{'}$ where $σ ⊑ σ^{'}$ , the same I may be used to discharge the existential, and S will be valid w.r.t $σ^{'}$ . □

4.3.3. Proofs of the propagation schema

Now we give a constructive proof of the propagation schema for $P_{l}$ . Recall that the computational content of the proof is a propagator for $P_{l}$ .

Theorem 13 ( $P_{l}$ Support Generation).

We consider $P_{l}$ on constraint $occurrenceleq (X, a, c)$ . We claim that Definition 19 (propagation schema) holds for $P_{l}$ .

Proof.
Let $σ_{1}$ and $σ_{2}$ be signatures mapping the variables in X to their respective domains. S and $σ_{1} ⊑ σ$ are universally quantified in the schema, therefore we use them as givens. We assume that $S \notin {support}_{⟨ X, σ_{1} ⟩} (P_{l})$ and prove the consequent by constructing $S^{'}$ and $σ_{2}$ . By lemma 12, $S \neq \emptyset$ . The second disjunct of $P_{l}$ would be satisfied by $S = \emptyset$ , therefore S corresponds to the first disjunct of $P_{l}$ .

S contains one literal for each index in I. At least one item in S is invalid (by the antecedant). The proof proceeds by constructing $I^{'}$ and corresponding $S^{'}$ and $σ_{2}$ to satisfy the first disjunct of $P_{l}$ if possible. Otherwise, the second disjunct is satisfied by constructing $σ_{2}$ and $S^{'} = \emptyset$ . $\begin{array}{l} I_{1} = {i ∣ ⟨ i, b ⟩ \in S \land (\exists b \neq a . b \in σ_{1} (X [i]))} \\ I_{2} = {i ∣ i \notin I_{1} \land (\exists b \neq a . b \in σ_{1} (X [i]))} \\ I_{3} = I_{1} \cup I_{2} \\ | I_{3} | > (| X | - c) \Rightarrow \\ (I^{'} \subseteq I_{3} \land | I^{'} | = (| X | - c + 1) \\ \land S^{'} = {⟨ i, b ⟩ ∣ i \in I^{'} \\ \land b \in σ_{1} (X [i]) \land b \neq a} \\ \land σ_{2} = σ_{1}) \\ | I_{3} | = (| X | - c) \Rightarrow \\ S^{'} = \emptyset \\ \land (\forall i \notin I_{3} . σ_{2} (X [i]) = σ_{1} (X [i])) \\ \land (\forall i \in I_{3} . σ_{2} (X [i]) = σ_{1} (X [i]) ∖ {a}) \end{array}$

$σ_{2}$ is maximal in both of the above cases: in the first case, $σ_{2} = σ_{1}$ , and in the second case only the necessary values are removed to satisfy the second disjunct of $P_{l}$ .

When $| I_{3} | < (| X | - c)$ , $P_{l}$ is false and remains false for all $σ_{2} ⊑ σ_{1}$ (by construction of $I_{1}$ and $I_{2}$ ). Hence the second disjunct of the consequent of the schema is satisfied. □

The proof explicitly re-uses variable indices but not b values from S. This fits well with Minion’s watched literal implementation, which notifies the propagator once for each invalid literal in S. However, the proof does not require the use of watched literals, it allows many concrete implementations and may be used with any propagation-based solver.

It is straightforward to prove the propagation schema for $P_{g}$ , based on the proof for $P_{l}$ .
Theorem 14 ( $P_{g}$ Support Generation).

We consider $P_{g}$ on constraint $occurrencegeq (X, a, c)$ . We claim that Definition 19 (propagation schema) holds for $P_{g}$ .

Proof.
The proof is the same as the proof of $P_{l}$ , with c substituted for $| X | - c$ in all places, and $(a \in σ_{1} (X [i]))$ substituted for $(\exists b \neq a . b \in σ_{1} (X [i]))$ , and ${a}$ substituted for $σ_{1} (X [i]) ∖ {a}$ . □

This proof also re-uses variable indices from S and thus fits well with Minion’s watched literal infrastructure.
4.3.4. Soundness and completeness

Now we prove the soundness and completeness of both properties, and hence the correctness of the two propagators.

Lemma 17 (Occurrenceleq Sound).

$\begin{array}{l} \forall σ . singleton (σ) \Rightarrow \\ ({support}_{⟨ X, σ ⟩} (P_{l}) \Rightarrow \\ {[[occurrenceleq (X, a, c)]]}_{σ} \neq \emptyset) \end{array}$

Proof.
Let σ be an arbitrary singleton signature. Since σ is a singleton it encodes a single tuple (say τ). Assume ${support}_{⟨ X, σ ⟩} (P_{l})$ holds. Let b be the number of occurrences of a in τ.

Since σ is singleton, the first disjunct of $P_{l}$ implies the second disjunct. (Assume I satisfies the first disjunct. $I^{'} \subseteq I$ where $| I^{'} | = (| X | - c)$ is used to satisfy the second disjunct.) Therefore ${support}_{⟨ X, σ ⟩} (P_{l})$ implies the second disjunct of $P_{l}$ is satisfied (by the empty support). Hence, at least $| X | - c$ elements of τ are not equal to a, so $b ⩽ c$ . By Definition 24 , $R_{X} = {τ}$ and the lemma holds. □

The proof that $P_{g}$ is sound proceeds by the same argument, with $| X | - c$ replaced with c, ‘not equal to a’ replaced with ‘equal to a’ and ⩽ replaced with ⩾.
Lemma 18 (Occurrenceleq Complete).

$\begin{array}{l} C = occurrenceleq (X, a, c) \\ \forall σ . {[[C]]}_{σ} \neq \emptyset \Rightarrow \\ \exists σ^{'} ⊑ σ . {[[C]]}_{σ} \subseteq {[[C]]}_{σ^{'}} \\ \land {support}_{⟨ X, σ^{'} ⟩} (P_{l}) \end{array}$

Proof.
Assume ${[[C]]}_{σ} \neq \emptyset$ for arbitrary σ. If ${support}_{⟨ X, σ ⟩} (P_{l})$ then $σ^{'} = σ$ and completeness trivially holds. Otherwise, by the proof of the propagation schema for $P_{l}$ , there exists a $σ^{'} ⊏ σ$ (named $σ_{2}$ there) such that ${support}_{⟨ X, σ^{'} ⟩} (P_{l})$ . Since $σ^{'} \neq σ$ , $σ^{'}$ is constructed in the case where $| I_{3} | = (| X | - c)$ . $σ^{'}$ is the same as σ except for indices $I_{3}$ , where the value a is removed if present. For all $i \notin I_{3}$ , $σ (i) = {a}$ therefore corresponding elements of all tuples $τ \in {[[C]]}_{σ}$ also equal a. No other element of τ can be a (by Definition 24), therefore no tuples are invalidated, ${[[C]]}_{σ^{'}} = {[[C]]}_{σ}$ and the lemma holds. □

Once again, the proof that $P_{g}$ is complete follows the same argument. For $P_{g}$ , $| I_{3} | = c$ and for all indices $i \in I_{3}$ , $σ^{'} (i) = {a}$ . For other indices, the constructed $σ^{'}$ is equal to σ and does not contain a. By Definition 25, all tuples $τ \in {[[C]]}_{σ}$ must equal a at all indices $I_{3}$ , therefore no tuples are invalidated under $σ^{'}$ and ${[[C]]}_{σ^{'}} = {[[C]]}_{σ}$ .
4.3.5. Empirical evaluation

The occurrence propagators implemented in Minion 0.12 use static triggers. Therefore they may be invoked when support has not been lost. By comparison, these watched literal propagators are only invoked when one of the literals in the support is lost.

We implemented the $occurrenceleq (X, a, c)$ propagator described by the proof of Theorem 13 in Minion 0.12. The propagator re-uses literals $⟨ i, b ⟩$ from S when constructing $S^{'}$ , allowing it to leave the corresponding watched literals in place. When a literal $⟨ i, b ⟩$ in S is invalid, the propagator scans through $X [{i \dots | X | - 1}]$ then $X [{0 \dots i - 1}]$ to find a replacement literal. The propagator (referred to as WatchedProp) was constructed from the proof in less than 3 hours programmer time.

We compare against the existing propagator for $occurrenceleq$ (StaticProp) provided in Minion 0.12, which uses static assignment triggers (i.e. the propagator is notified when any variable in scope becomes assigned).

We constructed a benchmark CSP as follows. We have a vector of variables X where $| X | = 100$ , and initial signature σ where $\forall i . σ (X [i]) = {1, 2}$ . The constraints are as follows: $\begin{matrix} \forall i \in {80 \dots 98} . (X [i] \neq X [i + 1]) \end{matrix}$ and 100 copies of the constraint: $\begin{matrix} occurrenceleq (X, 1, 90) \end{matrix}$ The occurrence constraint is duplicated to allow accurate measurement of its efficiency. This CSP is solved to find all solutions.

The solver branches on variables in X in index order, and branches for 1 before 2. Once variable $X [80]$ is assigned by search, the remaining variables are assigned by propagation on the ≠ constraints. As search progresses, the value of each variable in $X [{80 \dots 99}]$ alternates between 1 and 2.

WatchedProp watches 11 literals of the form $⟨ i, 2 ⟩$ . Early in the search, most of these literals will necessarily involve variables $X [{80 \dots 99}]$ , a pathological case for WatchedProp. As search progresses, more variables in $X [{0 \dots 79}]$ will be assigned 2, therefore the performance of WatchedProp should improve.

Table 1 shows that StaticProp scales approximately linearly in the number of search nodes explored, but WatchedProp speeds up as search progresses. With a limit of 100 million nodes, WatchedProp is more than twice as fast as StaticProp.

Table 1
Times for the WatchedProp and StaticProp algorithms, median of 16 runs on a dual processor Intel Xeon E5520 at 2.27 GHz

Search node limit (n) WatchedProp time (s) StaticProp time (s)

100,000 1.72 1.20

1,000,000 12.40 11.54

10,000,000 86.13 120.31

100,000,000 518.81 1205.07

Search node limit (n)	WatchedProp time (s)	StaticProp time (s)
100,000	1.72	1.20
1,000,000	12.40	11.54
10,000,000	86.13	120.31
100,000,000	518.81	1205.07

4.3.6. Discussion

We have shown that our framework can be used to create highly efficient watched literal propagators for occurrence constraints, and that these outperform conventional propagators that use static triggers. There is no requirement for the propagators to maintain GAC. In this case we have proven that the propagators are sound and complete, the most basic requirements for correctness. The framework is entirely agnostic about whether the propagator maintains GAC, some form of bound consistency or indeed some custom consistency that is specific to the type of constraint.

5. Conclusions and future work

This paper has made a number of contributions to the formal study of constraint solving, in particular of propagation in constraint solving. We have shown that we can define formally a notion of generalized support, which generalizes the standard notion of support in constraint satisfaction. This generalization allows us to work with propagators that might not have been seen as using support. Since our definition is so general, we introduced the notion of p-admissible support properties. The definition of p-admissibility corresponds to the use of a particular kind of trigger within the constraint solver. Triggers are events which cause propagators to be called within the solver, and p-admissibility guarantees that any event which might cause support to be lost is observed by some trigger. In this paper we have focussed on a definition of p-admissibility corresponding to literal triggers (that are activated by deletion of a particular value from the domain of a variable). We have given a formal description of constraint propagation. Given a p-admissible support property, we have defined the propagation schema. A constructive proof of the propagation schema shows how a propagator can be constructed to find new support when support is lost. We have given examples of this for the specific constraints element, occurrenceleq and occurrencegeq, and sketched an example for AllDiff.

Our work on propagators is not merely a formalisation of existing standard usage in constraint programming. We are not aware of a definition of support as general as ours within constraints. The notion of generalized support should be directly useful in constraints, enabling a much better understanding of propagation algorithms in the constraint community. Our hypothesis is that almost all propagators used in constraint solvers can be seen as reasoning with some form of support property, even though most propagators are not currently presented as doing so. Once this hypothesis is confirmed, we can present propagation algorithms in a much more uniform fashion, as well as building constraint solvers to exploit these propagation algorithms. Thus our intended future work consists of two strands: first continuing the formal development we have started here, and second demonstrating the application of our work to the constraints community.

Footnotes

Acknowledgements

The work of the authors has been partially supported by the following UK EPSRC grants: EP/E030394/1, EP/F031114/1, EP/H004092/1, and EP/M003728/1, support for which we are very grateful.

References

K.R.

Apt, Principles of Constraint Programming, Cambridge University Press, 2003. ISBN 0 521 82583 0. doi:10.1017/CBO9780511615320.

K.R.

Apt and

Monfroy, Automatic generation of constraint propagation algorithms for small finite domains, in: Proceedings of the Fifth International Conference on Principles and Practice of Constraint Programming (CP 1999), 1999, pp. 58–72.

Beldiceanu,

Carlsson,

Flener,

M.A.F.

Rodríguez and

Pearson, Linking prefixes and suffixes for constraints encoded using automata with accumulators, in: Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP 2014), 2014, pp. 142–157.

Beldiceanu,

Carlsson and

Petit, Deriving filtering algorithms from constraint checkers, in: Proceedings of the 10th International Conference on Principles and Practice of Constraint Programming (CP 2004), 2004, pp. 107–122.

Bessière, Constraint propagation, in: Handbook of Constraint Programming,

van Beek,

Rossi and

Walsh, eds, Elsevier, 2006, pp. 29–83.

Bessiere,

Hebrard,

Hnich and

Walsh, The tractability of global constraints, in: Proceedings of the 10th International Conference on Principles and Practice of Constraint Programming (CP 2004), 2004, pp. 716–720.

Bessière and

J.-C.

Régin, Arc consistency for general constraint networks: Preliminary results, in: Proceedings 15th International Joint Conference on Artificial Intelligence (IJCAI 97), 1997, pp. 398–404.

Bessière and

J.-C.

Régin, Refining the basic constraint propagation algorithm, in: Proceedings 17th International Joint Conference on Artificial Intelligence (IJCAI 2001), 2001, pp. 309–315.

Caldwell,

Gent and

Underwood, Search algorithms in type theory, Theoretical Computer Science 232(1–2) (2000), 55–90. doi:10.1016/S0304-3975(99)00170-X.

10.

D.A.

Cohen,

Jefferson and

K.E.

Petrie, A theoretical framework for constraint propagator triggering, in: Proceedings of the Ninth International Symposium on Combinatorial Search, 2016, pp. 19–27.

11.

R.L.

Constable, Naive computational type theory, in: Proof and System Reliability,

Schwichtenberg and

Steinbruggen, eds, Nato Science Series, Vol. 62, Kluwer, 2002, pp. 213–259.

12.

R.L.

Constable,

S.F.

Allen,

H.M.

Bromley,

W.R.

Cleaveland,

J.F.

Cremer,

R.W.

Harper,

D.J.

Howe,

T.B.

Knoblock,

N.P.

Mendler,

Panangaden,

J.T.

Sasaki and

S.F.

Smith, Implementing Mathematics with the Nuprl Proof Development System, Prentice Hall, 1986.

13.

E.C.

Freuder and

A.K.

Mackworth, Constraint satisfaction: An emerging paradigm, in: Handbook of Constraint Programming,

Rossi,

Van Beek and

Walsh, eds, Elsevier, 2006, pp. 13–28.

14.

I.P.

Gent,

Jefferson and

Miguel, MINION: A fast, scalable, constraint solver, in: Proceedings 17th European Conference on Artificial Intelligence (ECAI 2006), 2006, pp. 98–102.

15.

I.P.

Gent,

Jefferson and

Miguel, Watched literals for constraint propagation in Minion, in: Proc. 12th International Conference on the Principles and Practice of Constraint Programming (CP 2006), 2006, pp. 182–197.

16.

I.P.

Gent,

Miguel and

Nightingale, Generalised arc consistency for the AllDifferent constraint: An empirical survey, Artificial Intelligence 172(18) (2008), 1973–2000. doi:10.1016/j.artint.2008.10.006.

17.

J.-Y.

Girard,

Lafont and

Taylor, Proofs and Types, Cambridge University Press, 1989.

18.

IBM, IBM ILOG CPLEX Optimization Studio CP Optimizer User’s Manual Version 12 Release 6, 2015.

19.

Jefferson and

K.E.

Petrie, Provably pointless propagator calls, in: Fifth International Workshop on the Cross-Fertilization Between CSP and SAT, 2015, Co-located with CP 2015.

20.

M.J.

Maher, Propagation completeness of reactive constraints, in: Proceedings ICLP 2002, 2002, pp. 148–162.

21.

Prud’homme,

J.-G.

Fages and

Lorca, Choco3 Documentation, TASC, INRIA Rennes, LINA CNRS UMR 6241, COSLING S.A.S., 2014, http://www.choco-solver.org .

22.

J.-C.

Régin, A filtering algorithm for constraints of difference in CSPs, in: Proceedings 12th National Conference on Artificial Intelligence (AAAI 94), 1994, pp. 362–367.

23.

J.-C.

Régin, Generalized arc consistency for global cardinality constraint, in: Proceedings of the 13th National Conference on Artificial Intelligence (AAAI 96), 1996, pp. 209–215.

24.

Schulte and

P.J.

Stuckey, Efficient constraint propagation engines, ACM Transactions on Programming Languages and Systems (TOPLAS) 31(1) (2008).

25.

Smith, CSPLib problem 001: Car sequencing, CSPLib: A problem library for constraints, http://www.csplib.org/Problems/prob001.

26.

Tack,

Schulte and

Smolka, Generating propagators for finite set constraints, in: Proc. 12th International Conference on the Principles and Practice of Constraint Programming (CP 2006), 2006, pp. 575–589.

27.

Van Hentenryck,

Saraswat and

Deville, Design, implementation, and evaluation of the constraint language cc(FD), The Journal of Logic Programming 37 (1998), 139–164. doi:10.1016/S0743-1066(98)10006-7.

28.

Van Hentenryck,

Simonis and

Dincbas, Constraint satisfaction using constraint logic programming, Artificial Intelligence 58 (1992), 113–159. doi:10.1016/0004-3702(92)90006-J.

29.

Walsh, CSPLib problem 026: Sports tournament scheduling, CSPLib: A problem library for constraints, http://www.csplib.org/Problems/prob026.

Generalized support and formal development of constraint propagators

Abstract

Keywords

1. Introduction

1.1. Overview of the constraint satisfaction problem

1.2. Solving CSP

1.3. Proofs to propagators

1.4. Generalized support

1.5. Related work

2. Definitions and notation

2.1. The standard mathematical account

Definition 1 (Constraint Satisfaction Problem).

Definition 2 (Satisfying tuple).

Definition 3 (Solution).

2.2. Variable naming conventions, ranges, and literals

2.3. Vectors

2.4. Signatures

Lemma 1 (Signature Inclusion Well-founded).

2.5. Relations

2.5.1. Tuple coherency

Lemma 2 (Selection Wellformed).

2.5.3. Projection

Lemma 3 (Projection maps exist).

Corollary 1 (Tuple Projection Wellformed).

Notational Remark 1. Since projections Z where Z ⊆ X do not depend on the projection map they are built from when the X-tuple τ is coherent with Z, we will simply write Z ( τ ) in this case. Lemma 6 (Projection Coherent).

Definition 4 (Relation Projection).

Lemma 7 (Relation Projection WF).

2.5.4. Equivalence of constraints

Definition 5 (Schema Equivalence).

Definition 6 (Constraint Equivalence).

2.6. Syntactic definition of relations

Definition 7 (Semantics).

3. Propagation and support

Definition 8 (Generalized Arc Consistency).

Corollary 2 (Generalized Arc Consistency).

3.1. Support

Definition 9 (Support property).

Definition 10 (Support Set for a property P).

Definition 11 (Support for a collection of properties).

3.1.2. Admissible properties and triggers

Definition 12 (P-admissibility).

Definition 13 (Backtrack Stability).

Definition 14 (Properties True and False).

Lemma 8 (True singleton).

Lemma 9 (False Empty).

Corollary 3 (True and False are p-admissible).

Definition 15. We define the conjunction and disjunction of support properties as follows. ( P ∧ Q ) σ ( S ) = def P σ ( S ) ∧ Q σ ( S ) ( P ∨ Q ) σ ( S ) = def P σ ( S ) ∨ Q σ ( S ) We state the following lemma without proof. Lemma 10 (∧ and ∨ are p-admissible).

3.1.3. Extensional support for literals

Definition 16 (Support Property (for a Literal)).

Proof. Note that ⟨ i = a ⟩ does not refer to σ at all and so is p-admissible. □ 3.1.4. Generalized support – evidence

3.2. Soundness and completeness of a collection of propagators

3.2.1. Soundness

Definition 17 (Propagator Soundness).

3.2.2. Completeness

Definition 18 (Propagator Completeness).

Theorem 1 (Local Completeness).

3.3.1. The propagation schema

Definition 19 (Propagation Schema).

2 There is a classical proof of propagator schema that is independent of the property P and carries no interesting computational content.

Proof. Because property P is p-admissible, if we have ∅ ∈ support ⟨ X , σ ⟩ ( P ) then ∀ σ 1 ⊑ σ . ∅ ∈ support ⟨ X , σ 1 ⟩ ( P ) . □ 4. Generating propagators

4.1. A propagator for the element constraint

Definition 20 (Element Semantics).

Theorem 2 (Theorem 1 of reference [15]).

4.1.1. Support properties

Definition 21 (Element Support Properties).

3 This specification corresponds to a set of dynamic literal triggers [15]. Ideally a static assignment trigger would be used for P 1 , which would trigger the propagator when y is assigned. However, assignment triggers are outside the scope of this paper.

Lemma 13 ( P 1 is p-admissible).

Theorem 4 ( P 1 Support Generation).

Lemma 16 ( P e is sound).

4.2. Triggering the AllDifferent constraint

Definition 22 (AllDifferent Semantics).

Definition 23 (AllDifferent Support Property).

4.2.1. P-admissibility

4.2.2. Propagation schema, soundness and completeness

4.2.3. Discussion

4.3. New watched literal propagators for occurrence constraints

Definition 24 (Occurrenceleq Semantics).

Definition 25 (Occurrencegeq Semantics).

4.3.1. Support properties

Definition 26 (Occurrence Support Properties).

Notational Remark 1.
Since projections Z where $Z \subseteq X$ do not depend on the projection map they are built from when the X-tuple τ is coherent with Z, we will simply write $Z (τ)$ in this case.
Lemma 6 (Projection Coherent).

Proof.
Note that $⟨ i = a ⟩$ does not refer to σ at all and so is p-admissible. □
3.1.4. Generalized support – evidence

²
There is a classical proof of propagator schema that is independent of the property P and carries no interesting computational content.

Proof.
Because property P is p-admissible, if we have $\emptyset \in {support}_{⟨ X, σ ⟩} (P)$ then $\forall σ_{1} ⊑ σ . \emptyset \in {support}_{⟨ X, σ_{1} ⟩} (P)$ . □

4. Generating propagators

³
This specification corresponds to a set of dynamic literal triggers [15]. Ideally a static assignment trigger would be used for $P_{1}$ , which would trigger the propagator when y is assigned. However, assignment triggers are outside the scope of this paper.

Lemma 13 ( $P_{1}$ is p-admissible).

Theorem 4 ( $P_{1}$ Support Generation).

Lemma 16 ( $P_{e}$ is sound).

Theorem 10 ( $P_{l}$ is p-admissible).

Theorem 13 ( $P_{l}$ Support Generation).

Table 1
Times for the WatchedProp and StaticProp algorithms, median of 16 runs on a dual processor Intel Xeon E5520 at 2.27 GHz

Search node limit (n) WatchedProp time (s) StaticProp time (s)

100,000 1.72 1.20

1,000,000 12.40 11.54

10,000,000 86.13 120.31

100,000,000 518.81 1205.07