Typed Constraint Graph

In the heart of the NDL language lies a specific representation of the Constraint Programming Problems. Instead of using a common Constraint (Hyper-) Graph formalization, we introduce a Typed Constraint Graph (or TCG), that enriches the Constraint Graphs with types, representing the high level structure of the problem.

Typed Constraint Graph is a Labeled Directed Multigraph with no self-loops. Formally, it's an 8-tuple G = \left \langle V, A, s, t, \Sigma_V, \Sigma_A, l_V, l_A \right \rangle, where:

• V is a set of vertices representing variables and constants occurring in the problem
• A is a set of edges representing binary constraints occurring in the problem
• s and t are both maps A \rightarrow V pointing at the source and target vertices of an arc
• \Sigma_V is a set of the vertex labels
• \Sigma_A is a set of the arc labels
• l_V: V \rightarrow \Sigma_V maps vertices to their labels
• l_A: A \rightarrow \Sigma_A maps arcs to their labels

The following section will focus on semantics of the graph, most notably on the label sets and constraints that have to satisfied by the multigraph to be a Typed Constraint Graph

Typing

There are three kinds of types in the Typed Constraint Graph, two related to vertices, and one related to the arcs.

Sets

Set Type corresponds to a finite set of integers, as known from the MiniZinc language. Formally every Set is a tuple: \left \langle {ID}, {S} \right \rangle, where:

• ID is an unique type ID
• S is set of all integers inhabiting the type.

Inhabitant of the Set Type \left \langle {ID}, {S} \right \rangle is a pair \left \langle ID, c \right \rangle, where c \in S.

Variables

Variable Type corresponds to an array of Constraint Programming variables, as known from the MiniZinc language. Similarly to the arrays, inhabitants of the same Variable Type share domain and have unique indexes. Formally, every n-dimensional Variable Type is defined by a tuple \left \langle {ID}, \left \langle I_1, I_2, \ldots, I_n \right \rangle, {D} \right \rangle, where:

• ID is an unique type identifier
• I_k is a type ID of a Set used as the index set in the kth dimension
• D is a type ID of a Set, defining possible valuations of the type inhabitants

Inhabitant of the n-dimensional Variable Type \left \langle {ID}, \left \langle I_1, I_2, \ldots, I_n \right \rangle, {D} \right \rangle is represented by a n+1-tuple: \left \langle {ID}, i_1, i_2, \ldots, i_n \right \rangle, where i_k is an inhabitant of the corresponding I_k type.

Constraints

Constraint Type corresponds to a group of constraints occurring in the problem, grouped according to:

• aggregation functions (e.g. forall as in MiniZinc language),
• binary decomposition of global constraints used in the model.
  All constraints inhabiting the same Constraint Type share types of the arguments.

Constraint Type is represented as a tuple \left \langle {ID}, \theta_s, \theta_t \right \rangle, where:

• Id is unique type identifier
• \theta_s and \theta_t are type IDs of Variable/Set types, and represent what are the types of the constraint's arguments.

Constraints are not first order citizens of the NDL language, and are only used as the labels in the Typed Constraint Graph.

Labeling

Taking into consideration the types introduced in the previous section, the labeling of the Typed Constraint Graph is defined in the following way:

• \Sigma_V = \Sigma_\mathit{var} \cup \Sigma_\mathit{set}, where \Sigma_\mathit{var} contains all inhabitants of Variable types and \Sigma_\mathit{set} contains all inhabitants of the Set types defined in the problem
• \Sigma_A contains all Constraint Types defined in the problem
• l_V is an injective function
• the graph is well typed regarding to the constraints' arguments, i.e. \forall a \in A \left(l_A(a) = \left \langle ID, \theta_s, \theta_t \right \rangle \implies \theta(s(a)) = \theta_s \wedge \theta(t(a)) = \theta_t \right ), where \theta is a projection function mapping label to it's first element (type ID)

Additionally, for every Variable type identifier \mathit{id} we define a set of its' inhabitants \Theta_\mathit{id} = \left \{ \left \langle ID, I_1, \ldots I_n \right \rangle \in \Sigma_\mathit{var} : ID = \mathit{id} \right \}.

Neighborhood Definition Language

NDL language was designed to be a small Domain Specific Language, allowing to exploit information encoded in the Typed Constraint Graph to modify an existing problem solution in an intelligent manner.

Solution

Solution \mathit{sol} is an assignment of all the variables to the values from their corresponding domains. Set of all possible solutions will be written as \mathit{Sol}.

For every Variable type with identifer id, we define following set of functions to manipulate the solution:

• \mathit{get}: \mathit{Sol}, \Theta_{id} \rightarrow D(id)

Turing Incompleteness

Due to lack of unbounded recursion, the NDL is not Turing complete. Every program written in NDL is total and will always eventually end.

Independence from TCG

Programs written in the Neighborhood Definition Language are independent of the specific problem instance (specifically: domains, index sets and the TCG structure) and depend only on the types occurring in the problem, as the pattern matching refers to the labels in the underlying TCG.