Typed Constraint Graph

In the heart of the NDL language lies a specific representation of Constraint Programming Problems. Instead of using a common Constraint (Hyper-) Graph formalization, we introduce a Typed Constraint Graph, that enriches the Constraint Graphs with types, representing the higher 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 well 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 the 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 contains all inhabitants of Variable and 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)