Systematic Derivation of a Global Constraint for Routing

1 Global Constraints Based on Transfer Functions

Global constraints are a very efficient class of algorithms that can be used in local search, notably for routing optimization problems. Global constraints provide speed improvements compared to naive implementations because they perform some form of symbolic reasoning on the structure of the problem and exploit mathematical properties such as associativity and commutativity. They might however be time-consuming to develop.
The OscaR.cbls framework has a generic global constraint based on so-called transfer functions, which are used to label segments of routes [1], [2]. A transfer function F is a function T → T that can be either queried, as any function, or composed with another transfer function F ◦ F. The transfer function and the composition function together form a monoïd : the composition of two transfer function must be a transfer function. Both F and T are constraint-specific.
The generic global constraint precomputes all transfer functions involving the first and last node of a route. It also precomputes the transfer function in a logarithmic progression to label segments linking positions (0, 2),(2,4),(4,6),(6,8),... ; (0,4),(4,8),(8,16),... (0,8),(8,16),... etc. If the composition operator takes O(1)-time, this precomputation takes O(n)-time on a route of length n. On a 3-opt move, which creates four segments of the initial route, the transfer function of the first and last segments are available, and the transfer function of the two segments in the middle of the route are assembled out of O(log n) precomputed transfer functions. If the transfer function are evaluated in constant time, the constraint is updated in O(log n)-time.
To implement a new constraint base on this generic global constraint, one must define a transfer function and its associated composition operator. Although the framework hides away a lot of technicalities, this remaining task is challenging.

2 Systematic Derivation of Transfer Function and Composition Operator

To find the transfer function and the composition operator, one can follow an iterative "trial and error" approach, supported either by proof or by testing.
Alternatively, one can also follow a constructive approach, where the definition of the transfer function and composition operator are derived from the definition of the constraint. Derivation approaches are commonly found in formal methods such as B [3]. We could deploy such an approach on a complex constraint.
The considered constraint is a weighted tardiness constraint with early line. This constraint declares two classes of nodes : the first class takes part in a weighted tardiness ; the other class has an early line. Each node the of the first class has an associated weight. All nodes the of the second class share the same early line. For this constraint, we could derive the composition operator from the formal definition of the constraint.
We first crafted a transfer function for a single node. It is parameterized by the class of the node, its tardiness weight, and the early line. The transfer function has two inputs : the arrival time at the node and the summed tardiness of the preceding nodes ; and two outputs : the leave time from the node and the summed tardiness of this node and its preceding nodes. Then, a suitable transfer function for segments of route was crafted. It enriches the definition of the per-node transfer function with additional parameters. This enriched formula is -unfortunately- an educated guess.
The main task was to define the value of these parameters. This amounts to defining the composition operators. This is where the derivation process took place. We developed the formula obtained by chaining two transfer function algebraically. The resulting large formula was then re-arranged through distributiveness and associativity into the defined pattern of transfer function. Finally, we identified the terms of the resulting formula to the parameters of the transfer function. This defined the composition operator and proved that the transfer function and the composition operator together form a monoïd.
The derivation was performed in a single day. No subsequent demonstration was needed since the formula is correct by construction, and all tests passed immediately. This advocates that the derivation approach was relevant and cost efficient in this case.

Systematic Derivation of a Global Constraint for Routing

Acknowledgement : This work is supported by the Service Public de Wallonie Recherche under grant n°2010235 - TRAIL/ARIAC