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
, where:- is a set of vertices representing variables and constants occurring in the problem
- is a set of edges representing binary constraints occurring in the problem
- and are both maps pointing at the source and target vertices of an arc
- is a set of the vertex labels
- is a set of the arc labels
- maps vertices to their labels
- 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:
, where:- is an unique type ID
- is set of all integers inhabiting the type.
Inhabitant of the Set Type
is a pair , where .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
-dimensional Variable Type is defined by a tuple , where:- is an unique type identifier
- is a type ID of a Set used as the index set in the th dimension
- is a type ID of a Set, defining possible valuations of the type inhabitants
Inhabitant of the
-dimensional Variable Type is represented by a -tuple: , where is an inhabitant of the corresponding 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
, where:- is unique type identifier
- and 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:
- , where contains all inhabitants of Variable types and contains all inhabitants of the Set types defined in the problem
- contains all Constraint Types defined in the problem
- is an injective function
- the graph is well typed regarding to the constraints' arguments, i.e. , where is a projection function mapping label to it's first element (type ID)
Additionally, for every Variable type identifier
we define a set of its' inhabitants .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
is an assignment of all the variables to the values from their corresponding domains. Set of all possible solutions will be written as .For every Variable type with identifer
, we define following set of functions to manipulate the solution: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.