Wang Ruixin
email: ruixin.wang@enac.fr

Barnier Nicolas
email: nicolas.barnier@enac.fr

Propagation of Idle Times Costs for Fixed Job Scheduling

Keywords: job scheduling, robustness, optimization constraint

We present a new global constraint to propagate idle times costs for the Fixed Job Scheduling (FJS) problem, in particular to minimize their variance so as to optimize the robustness of solutions w.r.t. schedule deviations. The propagation of this constraint is based on the computation of the shortest path in the compatibility directed acyclic graph of each resource to obtain an exact lower bound. It ensures Bound Consistency on the resource cost in polynomial time, as well as the filtering of the resource variables associated with compatible tasks.

We show on tailored FJS problems and real instances of the airport Gate Allocation Problem (a variant of the FJS problem) that this new constraint provides significant improvements in terms of number of backtracks and computation time, up to orders of magnitude in some cases.

INTRODUCTION

Fixed Job Scheduling (FJS) [START_REF] Eliiyi | Heuristics for operational fixed job scheduling problems with working and spread time constraints[END_REF] is a well-known resource allocation problem with many applications where jobs (or tasks) with fixed start and end times are to be processed on different machines (or resources). Overlapping tasks must execute on different resources and the set of possible resources for a given task may be restricted. Standard objectives for the FJS problem include the maximization of the number of (possibly weighted) processed tasks or the minimization of the cost associated with assigned resources.

Normally, a task can only be executed according to a predefined schedule, but for applications like the Gate Allocation Problem (GAP) [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF] which aims at assigning airport stands to aircraft, the robustness of the plan should be optimized to absorb potential delays and avoid costly disruption. Despite its practical importance, the research on the robustness of solutions to the FJS problem or the GAP is very limited.

Following the robustness objective defined by [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF] that minimizes the variance of idle times to balance and spread them over time and resources, we show that this kind of model can be efficiently solved with Constraint Programming (CP). Our main contribution is a new optimization constraint on each resource that achieves Bound Consistency (BC) over its idle times costs in polynomial time, as well as the filtering of the allocation variables associated with possible tasks of the resource.

More standard objectives for the GAP includes the optimization of passengers walking distance [START_REF] Kim | Airport control through intelligent gate assignment[END_REF], the allocation of terminal gates over apron stands and minimization of the number of towing movements [START_REF] Guépet | Exact and heuristic approaches to the airport stand allocation problem[END_REF]. CP was also used to implement a solver that minimizes the allocation costs defined by airlines and the airport manager [START_REF] Simonis | Models for global constraint applications[END_REF]. Other search methods like Genetic Algorithms have been used as well in [START_REF] Bolat | Models and a genetic algorithm for static aircraft-gate assignment problem[END_REF] to improve the MIP approach presented in [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF].

The rest of the paper is organized as follows. We first present a mathematical formulation of the problem in section I, then describe a corresponding CP model in section II and the propagation of our new optimization constraint for idle times costs in section III. Section IV presents the results of our experiments on the FJS problem and the GAP with tailored and real data to assess the performances of our approach. The conclusion and further works are discussed in the last section.

I. FIXED JOB SCHEDULING

The scheduling of tasks with fixed start and end times on non-identical 1 resources is a versatile NP-complete problem [START_REF] Arkin | Scheduling jobs with fixed start and end times[END_REF] which occurs in many applications beside the GAP, like processors scheduling or staff rostering. Though various objectives can be associated with this problem, our approach is dedicated to optimize resource costs based on the idle times to ensure the robustness of solutions w.r.t. delays.

We present in the following sections the integer model used in our study (whereas more classical OR approaches rather consider boolean variables [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF]).

A. Instance

An instance of the FJS problem is defined by:

• T = {t 1 , . . . , t n } a set of n tasks, with ∀t i ∈ T :
t s i and t e i the start and end times of task t i ; -R i ⊆ R a set of compatible resources on which the task can be executed.

• R = {r 1 , . . . , r m } the set of m resources, with ∀r j ∈ R:

r s j and r e j the opening and closing times of resource r j . However, except when mentioned otherwise, all resources are considered available during the same period in the following, therefore ∀j, r s j = r s and r e j = r e .

-T j = {t i ∈ T s.t. r j ∈ R i } the set 2 of compatible tasks that can be executed on resource r j . For conciseness, we also define the duration function d, "overloaded" on the following sets:

• T → N the duration of a task: d(t i ) = t e i -t s i ; • 2 T → N the total sum of the durations of a subset of (possibly overlapping) tasks: d(T ) = ti∈T d(t i ); • R → N the availability of a resource: d(r j ) = r e j -r s j ; • 2 R → N the total sum of the availability of a set of resources: d(R ) = rj ∈R d(r j ).

B. Decision Variables

A solution to the fixed tasks scheduling problem consists in assigning a resource to each task while satisfying the constraints described in the next section. We define the set of decision variables associated to the tasks of T :

X = {x i ∈ {j s.t. r j ∈ R i }, ∀t i ∈ T } C. Constraints
The only constraints of this essential version of the problem are the non-overlapping of the tasks scheduled on the same resource. As tasks execution times are fixed, we require that overlapping tasks are assigned to different resources:

∀i = i , [t s i , t e i [∩[t s i , t e i [ = ∅ ⇒ x i = x i (1)
However, specific applications of the fixed tasks scheduling problem like the GAP are often described with many additional hard and soft constraints to account for operational requirements (e.g. a large aircraft might occupy two adjacent stands) or user preferences (e.g. use of terminal gates rather than remote apron stands).

D. Cost

Many different kind of costs can be taken into account to optimize the allocation of fixed tasks on non-identical resources. For our target application, the GAP, one of the most crucial objectives is the robustness of the schedule as air traffic operations can be burdened by many uncertainties such as late arrival or departure. To be able to absorb those possible delays, [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF] proposes to minimize the variance of idle times, which tends to balance them over resources and time while allowing necessary short or large pauses required by some instances.

Since their mean is constant for our problem (as the overall duration of tasks and availability of resources are constant, and all tasks must be scheduled), minimizing the variance of idle times amounts to minimizing the sum of their squares:

cost = rj ∈R c j
where c j is the cost of a single resource r j :

c j = (t s first(rj ) -r s j ) 2 + ti∈Tj s.t. xi=j (next(t i ) -t e i ) 2
2 Redundantly defined from R i to simplify notations in the next sections.

with:

• next(t i ) = r e j if t i is the last task assigned on resource r j or the start time of the task immediately following t i on r j otherwise;

• first(r j ) is the index of the first task scheduled on resource r j . However, our approach could be generalized to any objective that aggregates resource costs defined as a positive additively separable function of its idle times (or even the start and end times of its tasks).

II. CONSTRAINT PROGRAMMING MODEL

We present in this section how the previous formulation of the FJS problem translates in a CP context, similarly to the approach described in [START_REF] Simonis | Models for global constraint applications[END_REF]. We first describe how all maximal cliques of the interval graph can be easily computed to efficiently model the mutual exclusion of overlapping tasks, then how symmetry on resources and tasks can be broken, eventually focusing on idle times costs with the definition of a new global constraint named idlecost, the propagation rules of which are detailed in section III.

A. Constraints on Maximal Cliques

To specify the mutual exclusion constraints 1 on unitary resources, it would be sufficient to model each of them directly with a binary difference constraint. However, stronger propagations can be obtained with the well-known all-different global constraint on cliques of the associated interval graph, as noted in [START_REF] Simonis | Models for global constraint applications[END_REF]. Only constraints corresponding to all distinct maximal cliques need to be added, as any other clique would be subsumed by a maximal one.

In the general case, computing the maximum clique of an arbitrary graph is NP-Hard. However, [START_REF] Gupta | Efficient algorithms for interval graphs and circular-arc graphs[END_REF] mentions how all maximal cliques (including the maximum one) of an interval graph of n vertices can be generated by a sweep algorithm in Θ(n log n), or even linear time Θ(n) if the endpoints of the intervals are already sorted.

Indeed, once the 2n endpoints of the tasks are sorted by ascending order, all maximal cliques of the corresponding intersection graph can be easily detected by maintaining the list of overlapping tasks at each endpoints. While scanning the sorted list of endpoints, the corresponding task is added whenever its left endpoint is encountered and removed upon reaching its right endpoint.

For each minimal size of the maintained list (except when it is empty), a new clique can be started with all currently overlapping intervals, collecting all subsequently opened new intervals until a local maximum is reached, which corresponds to a new maximal clique. All-different constraints can then be posted in linear time on all maximal cliques to improve propagation and allow global reasoning over multiple resources.

However, a collection of all-different constraints that share subsets of variables and propagate independently may keep inconsistent values w.r.t. their conjunction. [START_REF] Simonis | Models for global constraint applications[END_REF] mentions the use of the non-overlap global constraint diffn introduced by [START_REF] Beldiceanu | Introducing global constraints in CHIP[END_REF], which was generalized to multiple dimensions and new propagation rules in [START_REF] Beldiceanu | Sweep as a generic pruning technique applied to the non-overlapping rectangles constraint[END_REF]. Nevertheless, it has been proved in [START_REF] Kutz | Simultaneous matchings: Hardness and approximation[END_REF] that the corresponding decision problem is NP-complete and it was deemed efficient enough to use a simple collection of alldifferent constraints in our model because the instances of our target application, the GAP, are relatively easy to solve w.r.t. the allocation problem, and because the objective, which is hard to optimize (see IV-B), does not depend on the makespan but on the even and balanced distribution of idle times.

B. Symmetry

Depending on the instance at hand, allocation problems may exhibit symmetries on equivalent resources and equivalent tasks. For the GAP, the former is much more frequent on real instances: many adjacent stands in a terminal share the same set of characteristics, whereas equivalent flights with the same aircraft type, company and dates are seldom. Breaking such symmetries often lead to drastic speed-up while proving optimality (see section IV).

1) Resources: Resources that have exactly the same set of possible tasks can be exchanged while preserving the admissibility and optimality of solutions. Therefore, whenever a (yet) unused resource is assigned to a task, all other unused equivalent resources should be removed from its domain upon backtracking.

To this end, all the equivalence classes C k of resources (with at least two elements) are computed before search. Before each assignment of a task i to an unused resource r j , we check if other unused resources remain in the corresponding class C to add the following goal:

(x i = r j ) ∨ (x i / ∈ {j s.t. r j ∈ C ∧ unused(r j )})
with predicate unused : T → B indicating whether a resource is still free of task or not.

2) Tasks: Two tasks i and i that have the same compatible resource set and arrival and departure dates can also be exchanged while preserving solutions. So they can be arbitrarily ordered with the following constraint:

∀i = i , (R i = R i ∧ t s i = t s i ∧ t e i = t e i ) ⇒ (x i < x i )
However, there is no occurrence of equivalent flights in the GAP data set used to assess the performance of our approach (see section IV-B).

C. Idle Times Cost

Modeling idle times costs with standard CP reification constraints would be cumbersome and inefficient. Therefore, we introduce a new global optimization constraint idlecost to tighten the bounds of the cost of a single resource and the domains of its possible tasks. In the following sections, we define the semantic of this constraint and static bounding schemes for the overall sum of all idle costs. Propagation rules for the idlecost constraint are then discussed in section III.

1) Optimization Constraint for a Single Resource: We introduce the idlecost optimization constraint on a single resource r j ∈ R to tighten its idle times cost and filter the resource variables of its set of possible tasks T j :

Definition 1 (The idlecost Constraint): Let X Tj ⊆ X be the set of resource variables associated to T j and f : N → N a non-decreasing elementary cost function that represents the contribution of a single idle time interval. The optimization constraint idlecost(r j , T j , X Tj , f, c j ) is satisfied iff:

• c j = f (t s first(rj ) -r s j ) + ti∈Tj s.t. xi=j f (next(t i ) -t e i )
with the first and next functions defined as in section I-D;

• the set of mutual exclusion constraints 1 of section I-C restricted to variables of X Tj is satisfied. 2) Static Lower Bound: A static lower bound for the overall sum of the squares of idle times can be easily computed as it is minimal when all idle times have the same size and are evenly distributed among all resources. For n tasks to be executed on m resources, there are exactly n + m idle time periods (taking the first and last idle times of every resource into account). Therefore, we can compute the following global lower bound for the objective:

cost ≥ (n + m) d(R) -d(T ) n + m 2 (2)
In many instances, the availability is identical for all resources, i.e. r s j = r s and r e j = r e , ∀j ∈ [1, m]. We can then benefit from the computation of the first and last maximal cliques K s and K e mentioned in section II-A to take into account necessary idle times before the execution of the tasks of the first clique and after the end of the tasks of the last one:

cost K = ti∈K s (t s i -r s ) 2 + ti∈K e (r e -t e i ) 2
As in 2, we can compute the duration of idle times corresponding to the lower bound of the objective for the tasks that does not belong to the first or last cliques, i.e. the total amount of idle times divided by the number of pauses n + m -k with k = |K s ∪ K e | (as the cliques might intersect if some tasks span from the first one to the last one):

idle LB = d(R) -d(T ) -idle K n + m -k with idle K = ti∈K s (t s i -r s ) + ti∈K e (r e -t e i )
. Therefore, we obtain the following tighter lower bound:

cost ≥ cost K + (n + m -k)idle 2 LB (3)
which can help reduce the optimality gap and prove solutions.

3) Static Upper Bound: For instances with identical availability for all resources, a simple upper bound could also be obtained by saturating the first resources except the last nonempty one (where tasks are stacked at the beginning). The corresponding bound would then be:

cost ≤ m d(r) 2 + (d(r) -k) 2 (4) with d(r) = r e -r s , m = m -d(R)-d(T ) d(r)
the number of empty resources and k = (d(R) -d(T )) mod d(r) the time taken by the tasks scheduled on the last non-empty resource. But this bound is very loose and not really significant to help close the optimality gap.

III. PROPAGATION OF IDLE TIMES COSTS

We present in this section a new polynomial algorithm to achieve Bound Consistency (BC) on the cost of a single resource for the idlecost constraint: after its execution, a partial assignment can be extended to the possible tasks of the resource such that the cost can be assigned either its lower or upper bound.

After describing a tight upper bound and a naive relaxed lower bound in section III-A, we introduce in more details our algorithm to achieve BC on the lower bound in section III-B. We define the following notations, used in these sections, w.r.t. a resource r j :

• T j = {t i ∈ T j s.t. j ∈ dom(x i )} its possible tasks; • T j = {t i ∈ T j s.t.
x i = j} its necessary tasks;

• ub j the upper bound induced by T j ;

• lb j the lower bound induced by T j and T j ; with dom(x i ) the set of currently possible values for x i .

A. Bounds Based on the Union of Tasks

In the next sections, we present simple algorithms to compute the upper bound and an approximation of the lower one.

1) Assignment and Upper Bound: The upper bound of a single resource can be computed thanks to the set of necessary tasks T j already assigned to r j . If the cost was linear, it would be enough to maintain the sum of the durations of the tasks of T j and subtract it from the availability of the resource to obtain a tight upper bound on the cost: d(r j ) -ti∈Tj d(t i ). Upon assignment of a task t i , we would just have to subtract its duration to incrementally maintain the bound in constant time:

ub j ← ub j -d(t i ).
Though for a positive non-linear cost like the sum of the squares of idle times, we have to thoroughly maintain the set of idle intervals to be able to determine which one will be impacted by the new assigned task t i , and compute the new upper bound incrementally. Once the idle interval [a, b[ is identified, the upper bound is updated accordingly:

ub j ← ub j -(b -a) 2 + (t s i -a) 2 + (b -t e i ) 2 (5)
As T j only contains disjoint tasks, a simple binary search tree could be used to maintain the set of intervals and update the upper bound in logarithmic time upon assignment, provided that the data structure be easily "backtrackable". However, considering the low number of tasks associated with each resource in the instances of our target application (the GAP, cf. section IV-B), we only implemented a simple linear algorithm in the solver presented in section IV to avoid the likely overhead costs of a more sophisticated data structure. Fig. 1. The resource and tasks of example 1 with unbounded lower bound approximation ratio.

2) Removal and Lower Bound: The removal is not as straightforward as the assignment because tasks are not disjoint within T j , so the removal of one task from a resource r j does not entail that a new necessary idle time appears on r j . However, by maintaining the union of intervals corresponding to the tasks of T j , necessary idle times can be detected whenever T j does not span the entire availability. The lower bound can then be updated as follows upon a task removal:

lb j ← l k=1 (h e k -h s k ) 2 (6)
with

H j = [r s j , r e j [ \ ∀ti∈Tj [t s i , t e i [= l k=1 [h s k , h e k [
the necessary "holes" (possibly ∅, in which case lb j ← 0).

A segment tree data structure [START_REF] Berg | Computational Geometry: Algorithms and Applications[END_REF] can be used to maintain the tasks intervals, and augmented to also aggregate the upper bound of each subtree, including the root node which holds the bound for the whole resource, in Θ(k log n) with n the number of intervals and k the number of newly discovered necessary idle times. However, for reasons already mentioned in the previous section, our solver only use a naive (but simple) quadratic algorithm.

B. Tight Lower Bound

Among the bounds presented in the previous section, only the upper one is tight, because the assignment of a new possible task on a resource necessarily decreases the cost. In contrast, the lower bound is not, as the union of tasks doesn't take into account temporal conflicts. Therefore, the actual lower bound could be arbitrarily larger as, for example, with the following set of n possible tasks on a given resource depicted in figure 1:

Example 1 (Overlapping tasks with unbounded lower bound approximation ratio): ∀i ∈ [0.. n 2 -1]:

• t s 2i+1 = 2i(g + 1)
and t e 2i+1 = 2i(g + 1) + g + 2 • t s 2i+2 = (2i+1)(g +1) and t e 2i+2 = (2i+1)(g +1)+g +2 with r s = 0, r e = n(g + 1) + 1 and some constant g ∈ N >0 . The lower bound of section III-A applied to example 1 would be 0 whereas the actual lower bound is n 2 g 2 . Therefore, the ratio of the actual lower bound over the one defined by equation 6 can be arbitrarily large.

To achieve BC on the cost lower bound, the best admissible solution for the single resource should be taken into account. This best solution must be a maximal independent set of the conflict graph, as adding another task can only decrease the cost of a resource, but it is not necessarily either the maximum independent set (as the number of tasks is not relevant on instances with different durations) or even the largest (duration wise) maximal one as it would be the case with a linear cost.

More precisely, a solution corresponding to the lower bound must be a shortest path between fictive vertices v 0 and v n+1 corresponding to the opening and closing of the resource in the weighted compatibility Directed Acyclic Graph (DAG) G = (V, E) of the n possible tasks of resource r j :

• V = {v i , ∀t i ∈ T j } ∪ {v 0 , v n+1 } • E = {(v i , v i ) s.t. t e i ≤ t s i } • w : E → N with w((v i , v i )) = (t s i -t e i ) 2
with t e 0 = r s and t s n+1 = r e . Note that any positive function could be used to weigh the idle times instead of their square.

In a DAG, the shortest path between two vertices can be computed in linear time Θ(|V | + |E|) [START_REF] Cormen | Introduction to Algorithms[END_REF], provided a topological ordering of the vertices (corresponding to the tasks sorted by increasing start time). Therefore, the lower bound of an idlecost optimization constraint can be computed in linear time with respect to G (i.e. possibly quadratic time w.r.t. the number of tasks n):

lb j ← dist(v 0 , v n+1 ) (7)
with dist : V 2 → N the length of the shortest path from v 0 to v n+1 in G.

After the initialization steps where T j and G are built and the bounds computed, the idlecost constraint must propagate whenever:

• A task t i is assigned to r j :

the upper bound must be updated (cf. section III-A); the arcs of the predecessors of v i pointing to vertices v i s.t. i > i (i.e. that "skip" v i ) must be deleted; if v i does not belong to the previous shortest path, a new one must be computed and the lower bound updated accordingly.

• A task t i is removed from r j :

the arcs of the predecessors of v i pointing to v i must be deleted; if v i belongs to the previous shortest path, a new one must be computed and the lower bound updated accordingly. Moreover, thanks to the previous tightening algorithms, we are also able to filter the domains of the decision variables corresponding to tasks of T j whenever the bounds of the resource cost variable c j are updated:

• If the upper bound c j of c j is modified:

if c j < lb j , a failure is triggered; if c j < ub j , we try to determine if some tasks of T j \T j (i.e. the set of possible tasks not yet assigned) must be added: for each task t i of this set, if its removal entails a new lower bound lb j s.t. lb j > c j , then the task must be assigned to r j , i.e. x i = j.

• Conversely, if the lower bound c j of c j is modified:

if c j > ub j , a failure is triggered; if c j > lb j , we try do determine if some unassigned tasks must excluded from r j : if the addition of a task entails a new upper bound ub j s.t. ub j < c j , then the task must be excluded from r j , i.e. x i = j.

Note that all the modifications of the maintained data structures induced by these tests must systematically be undone.

To sum up, the idlecost optimization constraint achieves the BC on the cost of a single resource and the filtering of the resource variables of its possible tasks in:

• O(n 2 ) when a task is assigned: O(log n) to update the upper bound, O(n 2 ) to delete the bypassing edges of the DAG and O(n 2 ) to find a shortest path; • O(n 2 ) when a task is removed: O(n) to delete edges and O(n 2 ) to compute the shortest path; • O(n 3 ) when the upper bound of c j is modified: O(n) shortest path to compute; • O(n 2 log n) when the lower bound of c j is modified:

there might be O(n) uncovered idle times at most for the O(n) tasks. The overall propagation algorithm has then a worst-case time complexity in O(n 3 ). However, most of the time, the propagation events and the structure of the compatibility DAG of the resource at a given node will not trigger the necessary conditions to meet this worst case.

Nonetheless, the computation of shortest paths, involved in the most costly rules, can also be implemented incrementally. Each time a task t i is assigned on the resource, let t i and t i be the preceding and succeeding assigned tasks (possibly t 0 and t n+1 ) w.r.t. t i , then only the shortest path between v i and v i needs to be recomputed (therefore the lower bound can be updated incrementally), and the shortest path problem is divided into two independent subproblems between v i and v i , and v i and v i . The results presented in section IV were obtained with this incremental algorithm, not detailed here for the sake of brevity.

IV. RESULTS

We report in this section the performances of the various techniques described in sections II and III to solve the FJS problem, especially the BC version of the idlecost constraint, implemented with the FaCiLe CP OCaml library [START_REF] Barnier | FaCiLe: a Functional Constraint Library[END_REF].

We first show how the incremental BC version of the idlecost constraint (named BC-IC) described in section III-B largely outperforms the approximate one (named AP-IC) presented in section III-A2 on a specific class of instances. Then we compare the two versions on instances of the GAP extracted from real data, as well as the effect of symmetry breaking (cf. section II-B) and incremental maintenance of the shortest path mentioned at the end of section III-B. An ad hoc search strategy that balances the workload over resources and selects the best task w.r.t. the idle times cost was used throughout the tests.

All the experiments were carried out on an AMD Ryzen 1920X at 3.5GHz with 32GB of RAM, running GNU/Linux kernel 4.15 and OCaml 4.05.0 compiler. Note that all execution time and backtracks amount graphs are plotted with a base 10 logarithmic scale, with the AP-IC version in red and the BC-IC one in green, dashed lines corresponding to the discovery of the optimal solution and plain ones to its proof.

A. Structured Problem

To assess the benefit of the BC version of the idlecost constraint over the approximate one, we have tailored instances that generalize the class presented in example 1 for several resources. As shown in figure 2, the tasks of the instances are structured like successive "stairs" with m resources and n = km tasks, which leads to an obvious optimal solution with one resource per level. As in example 1, the exact lower bound k -1 computed by BC-IC, can be arbitrarily better than the null value of its AP-IC counterpart.

Figures 3 and4 respectively compare the resolution time and amount of backtracks to prove optimality for AP-IC and BC-IC with an increasing number of resources and k = 4 (i.e. 4 tasks per resource). The BC-IC version systematically outperforms the AP-IC one, up to 8 times better for the number of backtracks and 3 times better for the optimality proof, showing that the extra effort to compute an exact lower bound pays off on this class of instances.

B. Application to the Gate Allocation Problem

The GAP mainly focus on finding an allocation of a given set of aircraft with fixed occupancy periods to a number of gates. If there was no compatibility restriction, this decision problem could be modeled as the coloring of an interval graph, which is polynomial [START_REF] Gupta | Efficient algorithms for interval graphs and circular-arc graphs[END_REF]. But gates can only accept a restricted set of aircraft types, so the set of compatible gates for an aircraft is limited and the decision problem of the allocation is rather a list-coloring problem, which is NP-Complete [START_REF] Biró | Precoloring extension. I. Interval graphs[END_REF]. Moreover, an aircraft with scheduled arrival and departure times can be considered as a task with fixed start and end times, and a gate as a specific resource. The GAP can therefore be considered as a FJS problem as defined in section I. However, gates are endowed with many other secondary features (e.g. compatible airlines, domestic/international, terminal/remote etc.) which should match the characteristics of the flight and the preferences of airlines as much as possible. These preferences can be modeled as costs (or soft constraints) associated with each possible assignment, and standard GAP objectives usually aim at minimizing their sum, which is NP-Hard [START_REF] Kroon | The optimal cost chromatic partition problem for trees and interval graphs[END_REF]. Other classic objectives include the walking distance of passengers or other connection means (e.g. buses), and there can be many side constraints like the simultaneous occupancy of adjacent gates for large aircraft.

As proposed by [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF], we focus here on optimizing the robustness of the overall schedule, in order to absorb possible deviations from the original schedule due to traffic delays, severe weather conditions or equipment failures. Hence, the GAP version presented here is a FJS problem with an additively separable objective on the idle times (as mentioned in section I-D). Nevertheless, as our model is a CP one, many of the aforementioned side-constraints or objectives could be added easily.

In the following, we compare the performances of the AP-IC and BC-IC versions of the idlecost constraint on instances extracted from real traffic on a busy airport from 09:00 to 18:00. The instances are randomly built from small subsets of all the airport gates in order to obtain optimality proofs in reasonable time. An example of the Gantt diagram of an optimal solution is shown on figure 5 for an instance with 7 gates and 35 aircraft. We show as well the benefits of symmetry breaking on gates and incremental maintenance of the shortest path used by BC-IC.

1) AP-IC vs BC-IC: Figures 6 and7 shows the number of backtracks and execution time to find and prove an optimal solution when using AP-IC and BC-IC for instances of the GAP with 7 gates (as in figure 5) w.r.t. the number of aircraft. BC-IC systematically outperforms AP-IC, especially in terms of backtracks which can differ by orders of magnitude.

2) Symmetry Breaking: As mentioned in section II-B, instances of the FJS problem (and the GAP) may present symmetry on equivalent resources or tasks (rarely for the GAP). Figures 8 and9 present the number of backtracks and execution time to find and prove an optimal solution for the instances described in section IV-B1, with and without symmetry breaking on gates. As expected, the proof of optimality can be obtained orders of magnitude faster with symmetry breaking for the instances considered, and the optimal solution may be reached sooner for particularly hard instances with enough symmetry.

3) Incremental Maintenance of the Shortest Path: As mentioned in section III, the shortest path of the compatibility DAG used by IC-BC when the idlecost constraint propagates can be computed incrementally, by restricting the shortest path to subproblems between fixed tasks. Figure 10 shows the execution time for the instances described in section IV-B1, with and without the incremental maintenance of the shortest path. The more sophisticated incremental algorithm consistently outperforms the simpler version based on the recomputation of the shortest path by approximately 10%.

CONCLUSION AND FURTHER WORKS

In this article, we present a new global constraint to improve the efficiency of CP solvers to find and prove robust solutions to the FJS problem that minimize the variance of idle times as proposed by [START_REF] Bolat | Procedures for providing robust gate assignments for arriving aircrafts[END_REF]. This new optimization constraint, named idlecost, ensures the Bound Consistency of the idle times cost associated with each resource and the filtering of the resource variables associated with each possible task. In particular, we use a O(|V | + |E|) shortest path algorithm on the compatibility DAG of the possible tasks to compute an exact lower bound for the cost of each resource and to include tasks when their removal would be incompatible with the current upper bound of the cost. We show that our approach consistently outperforms more naive approximations, sometimes by several orders of magnitude, for tailored structured problems and instances of the GAP extracted from real traffic.

We describe as well several useful techniques that improve resolution time like the computation of all maximal cliques of the interval graph to ensure mutual exclusion of overlapping tasks, the computation of global lower and upper bounds, the symmetry breaking on equivalent gates which helps to prove optimal solutions and sometimes to find them, and the incre-mental maintenance of the shortest path of the compatibility DAG at the core of our new optimization constraint. Furthermore, our solver could benefit from additional refinements like the global processing of several all-different constraints [START_REF] Lardeux | Interleaved alldifferent constraints: CSP vs. SAT approaches[END_REF] or the computation of a better, possibly dynamic, global lower bound to refine the one presented in this article. Our CP approach could also be hybridized with a MIP solver to improve its efficiency, or meta-heuristics to handle larger instances. Eventually, other standard objectives for the GAP, including the gate occupancy rate or allocation costs (corresponding to airlines and airport manager preferences), and side constraints (e.g. large aircraft may occupy two adjacent stands) could easily be added within our model.

Fig. 2 .

 2 Fig. 2. Structured problem with m resources and n = km tasks.

Fig. 3 .

 3 Fig. 3. Number of backtracks needed by the AP-IC and BC-IC versions to prove optimality for the structured problem w.r.t. the number of resources and with k = 4.

Fig. 4 .

 4 Fig. 4. Execution time (in seconds) corresponding to the number of backtracks of figure 3.

Fig. 5 .Fig. 6 .

 56 Fig. 5. Gantt diagram (in hours) of an optimal solution for an instance of the GAP with 7 gates and 35 aircraft extracted from real traffic.

Fig. 9 .Fig. 10 .

 910 Fig. 9. Execution time (in seconds) corresponding to the number of backtracks of figure 8.

Note that with identical resources (i.e. all tasks can be assigned to any resource), this problem becomes equivalent to the coloring of an interval graph, which is polynomial[START_REF] Gupta | Efficient algorithms for interval graphs and circular-arc graphs[END_REF].


Olivier Hermant
email: olivier.hermant@mines-paristech.fr

Polarized Rewriting and Tableaux in B Set Theory

We propose and extension of the tableau-based first-order automated theorem prover Zenon Modulo to polarized rewriting. We introduce the framework and explain the potential benefits. The first target is an industrial benchmark composed of B Set Theory problems.

Introduction

The B Method set theory [START_REF] Abrial | The B-book: Assigning Programs to Meanings[END_REF] has been extensively used for 20 years by the railway industry in France to develop certified correct-by-construction software. Recently, the BWare [START_REF]The BWare Project[END_REF] project has tackled the issue of automatically proving the thousands of proof obligations generated by the development process.

Zenon Modulo [START_REF] Delahaye | Zenon modulo: When achilles outruns the tortoise using deduction modulo[END_REF] is one of the tools developed to this aim. Originally a tableau-based prover, Zenon [START_REF] Bonichon | Zenon : An extensible automated theorem prover producing checkable proofs[END_REF] is used for instance by TLA+ [START_REF] Cousineau | TLA + proofs[END_REF] and FoCaLiZe [START_REF] Dubois | Verified functional iterators using the focalize environment[END_REF]. To help manage the axioms of set theory, but also the uncountable derived constructs definitions (e.g. inclusion, union, functions), we deemed useful to not let nonlogical axioms wander as formulas: a prover would easily get lost by decomposing one or another axiom in an unorganized fashion.

We replaced them with rewrite rules, turning Zenon into an implementation of Deduction Modulo Theory [START_REF] Bonichon | TaMeD : A tableau method for deduction modulo[END_REF][START_REF] Bonichon | A semantic completeness proof for tableaux modulo[END_REF][START_REF] Dowek | Theorem proving modulo[END_REF], which allows rewriting on terms and formulas. Additionally, we equipped it with ML polymorphic types and arithmetic [START_REF] Bury | Automated deduction in the B set theory using typed proof search and deduction modulo[END_REF]. On the BWare benchmark, the success rate was raised from 2.5% to 95%.

We propose to extend Zenon Modulo with polarized rewriting, a more permissive rewrite relation. We first introduce the framework, then we discuss examples and the pros and cons of the approach. There is currently no implementation, essentially because this is a perfect match for an intern or a PhD student.

Polarized Tableaux Modulo Theory

We assume familiarity with first-order logic and at least one deduction system. Tableaux calculus is a refutational calculus, thus, to show F under the assumptions Γ , we refute Γ, ¬F . The first-order tableaux rules are recalled in Figure 1, see textbooks [START_REF] Nerode | Logic for Applications[END_REF] for details. The rules have the following characteristics:

as customary, they are presented in a top-down fashion.

-Formulas are not in negation normal form, rules are duplicated.

-A branch may be closed, denoted ⊙, if we find on it (including internal nodes) an occurrence of some F and its negation, or an explicit contradiction. A tableau is a proof iff each branch is closed. -α-rules are for non-branching connectives rules and β-rules for branching ones, δ-rules are for quantifier rules introducing a fresh constant c and γrules for those introducing any term.

⊥ ⊙ ⊥ ⊙ F, ¬F ⊙ ⊙ ¬⊤ ⊙ ¬⊤ ⊙ ¬¬F ᬬ F F ∧ G α∧ F, G ¬(F ∨ G) α¬∨ ¬F, ¬G ¬(F ⇒ G) α¬⇒ F, ¬G F ∨ G β∨ F | G ¬(F ∧ G) β¬∧ ¬F | ¬G F ⇒ G β⇒ ¬F | G ∃x F (x) δ ∃ F (c) ¬∀x F (x) δ ¬∀ ¬F (c) ∀x F (x) γ ∀ F (t) ¬∃x F (x) γ ¬∃ ¬F (t)
Fig. 1: Tableaux Rules Tableaux Modulo Theory [START_REF] Bonichon | TaMeD : A tableau method for deduction modulo[END_REF] extends tableaux with a set of rewrite rules R. A rewrite rule is a pair of terms, l → r, where the variables of r appear in l. Given a set R, a term t rewrites into u, denoted t → u, if there is a rule l → r ∈ R and a substitution σ, such that there is an occurrence of lσ in t, and u is t where that occurrence has been replaced with rσ. In other words, → is the closure of R by substitution and the subterm relation. The transitive closure of → is denoted ։ and its further reflexive-symmetric closure is ≡, which is a congruence.

Deduction Modulo Theory also allows rewrite rules on formulas, provided the left member P of such a rule P → F is atomic. The relations →, ։, ≡ on formulas embed their counterparts on the subterms of the formulas.

Tableaux can be extended to rewriting with the addition of a rule allowing to convert any formula with ≡, as in Figure 2a. When rewriting is confluent, we can orient this rule as in Figure 2b. In practice, Deduction Modulo Theory-based automated theorem provers [START_REF] Burel | Embedding deduction modulo into a prover[END_REF] implement this last rule, which is a way to decide ≡ when confluence holds. Other presentations exist [START_REF] Bonichon | TaMeD : A tableau method for deduction modulo[END_REF][START_REF] Bonichon | A semantic completeness proof for tableaux modulo[END_REF][START_REF] Bury | Automated deduction in the B set theory using typed proof search and deduction modulo[END_REF].

The calculus of Zenon Modulo [START_REF] Bury | Automated deduction in the B set theory using typed proof search and deduction modulo[END_REF] enjoys meta-variables, Hilbert's ǫ operator, reasoning over reflexive/transitive/symmetric relations, an equality predicate, ML-polymorphic types, and, of course, rewriting. The simpler case of Figure 1 is sufficient here, as we focus on rewriting, that we now extend to polarity.

F ≡ , if F ≡ G G (a) General Case F ։ , if F ։ G G (b) Confluent Case
-G is F , -G is G 1 ∧ G 2 , G 1 ∨ G 2 , ∀xG 1 , ∀xG 1 or H ⇒ G 1 and the occurence of F in G 1 or G 2 is positive (resp. negative), -G is ¬G 1 or G 1 ⇒ H and the occurrence of F in G 1 is negative (resp.
positive).

Now, we consider two (proposition) rewrite systems R + ∪ R -.

Definition 2 (Polarized Rewrite Relation). Let F and G be two formulas. F → + G iff F → G with a term rewrite rule or there exists a positive (resp. negative) occurrence H in F , a substitution σ, and a rule l → r ∈ R + (resp. R -), such that H = lσ and G is F where H has been replaced with rσ. F → -G iff ¬F → + ¬G, that is to say we exchange R + and R -above.

We denote by ։ + and ։ -the reflexive-transitive closures of → + and → -, respectively. Defining ≡ + and ≡ -is more delicate and unlikely to be useful practice. Polarized Tableaux combine the rules of Figure 1 and Figure 3.

F ։+ , if F ։+ G G

Implementation

Zenon Modulo rewrites only literals, in a forward fashion. This is a further restriction of Figure 2b and it relies on termination of term rewriting and on confluence of the whole rewriting. Otherwise, completeness of the proof search fails. The heuristic is, each time we meet a literal, to:

1. normalize the terms it contains; 2. rewrite the literal itself (if there is an applicable rewrite rule) on one step; 3. if the formula is in normal form or compound, stop, otherwise repeat.

To get polarized rewriting it suffices to modify the second step into "rewrite positively if the literal is positive, negatively otherwise". The expected gain does not lie here, but in an optimized preprocessing for rules. Indeed [START_REF] Dowek | Polarized deduction modulo[END_REF], a polarized rule P → + F ∈ R + represents/can be represented as an axiom ∀(P ⇒ F ) (∀ is the universal closure over the free variables). Similarly, a negative rewrite rule P ։ -F ∈ R -is equivalent to the axiom ∀(F ⇒ P ). In contrast, Deduction Modulo Theory's rewrite rules P → F are equivalent to ∀((P ⇔ F ) [START_REF] Dowek | Theorem proving modulo[END_REF]. Remind that we are discussing propositional rewrite rules, so P has to be atomic. Consequently, polarization offers the following improvements:

more axioms correspond to rewrite rules, and this improves proof search [START_REF] Delahaye | Zenon modulo: When achilles outruns the tortoise using deduction modulo[END_REF].

Axioms of the form ∀x(P ⇒ A) and ∀x(A ⇒ P ), with P atomic, become rules of R + and R -, respectively. In classical logic, when P is a negated atom, we also get rewrite rules in R -and R + , respectively. -We can Skolemize rewrite rules. This has two benefits: first, less inference rules are necessary in the tableaux, and second, the Skolem term is uniform, while multiple applications of δ ∃ or δ ¬∀ introduce different fresh symbols at each time. This also holds in the presence of meta-variables.

Skolemizing the rules is impossible in vanilla Deduction Modulo Theory, as rewriting applies at positive and negative occurrences. Therefore, we do not know in advance which quantifiers are positive and negative. To illustrate the difference, consider axioms of the type ∀x(P ⇒ A) and ∀x(A ⇒ P ).

-In ∀x(P ⇒ A), we can replace all the positive existential and negative universal quantifiers of A by a Skolem function symbol. -Similarly, in ∀x(A ⇒ P ), we can replace all the positive universal and negative existential quantifiers of A by a Skolem function symbol.

The very same principle applies to polarized rewrite rules. We leave the study and the choice of the strategies for Skolemization [START_REF] Nonnengart | Computing small clause normal forms[END_REF] for a later stage. Both improvements can be applied to heuristics turning assumptions (of a given problem) into rewrite rules, and to hand-tuning of the rewrite rules of a specific theory, for instance B Method set theory.

Example

Let us consider the classical example of proving a ⊆ a with the standard axiom of inclusion ∀x∀y x ⊆ y ⇔ (∀z z ∈ x ⇒ z ∈ y). A usual tableau proof involves the succession of rules γ ∀ (twice), α ∧ , β ⇒ , δ ¬∀ and α ¬⇒ on the axiom. Deduction Modulo Theory turns it into the rewrite rule x ⊆ y → (∀z z ∈ x ⇒ z ∈ y), and yields the 3-rules axiomless proof of Figure 4a.

If we switch to Polarized Deduction Modulo Theory, we get the pair

R + = {x ⊆ y → (∀zz ∈ x ⇒ z ∈ y)} and R -= {x ⊆ y → (f (x, y) ∈ x ⇒ f (x, y) ∈ y)}.
The proof of a ⊆ a is one more step smaller, as shown in Figure 4b.

¬(a ⊆ a) ։ ¬(∀z z ∈ a ⇒ z ∈ a) α ¬∀ ¬(c ∈ a ⇒ c ∈ a) α¬⇒ ¬(c ∈ a), c ∈ a ⊙ ⊙ (

Conclusion

We expect the polarized approach to give at least as efficient as Zenon Modulo itself. The proof-search algorithm needs only few changes, mostly in the rule pre-processing. The obtained rules contain less quantifiers, allowing for fewer rules in proof-search and potential earlier unification and branch closure, since using a rewrite rule several times now involves the same Skolem symbol. On the risk side, implicational axioms can now be turned into rewrite rules. This might be a threat to termination or confluence. A study of the theoretical framework, including models, is required. Automated theorem provers are aggressively optimized tools, naturally lending themselves to bugs. This is why independent double checking facilities are important. Zenon Modulo is able to produce proof-terms or proof certificates, though it provides no rewrite steps explicitly, following Poincaré's Principle: computations (rewriting) in proofs give no insight, they can be quickly reconstructed (by the checker) at will and are to be left implicit. Such a clerk/expert distinction has for instance been studied in the Foundational Proof Certificate project [START_REF] Miller | Foundational proof certificates[END_REF], at the proof level, with the help of focusing [START_REF] Chihani | A semantic framework for proof evidence[END_REF].

On the BWare benchmark, all statements proved by Zenon Modulo [START_REF] Bury | Automated deduction in the B set theory using typed proof search and deduction modulo[END_REF], that do not involve arithmetic, are actually declared well-typed by Dedukti [START_REF] Boespflug | The λΠ-calculus modulo as a universal proof language[END_REF], a type checker based on an extension of Deduction Modulo Theory to dependent types. Dedukti's rewriting ability made extremely smooth the reconstruction of rewriting : there is essentially nothing to do but to declare the rules.

The challenge is to keep this skeptical double-checking approach viable. We may need a depolarization of the proofs, perhaps following [START_REF] Burel | Regaining cut admissibility in deduction modulo using abstract completion[END_REF], or an substantial extension of Dedukti and its foundations to polarized rewriting, perhaps with the help of subtyping.

Fig. 2 :

 2 Fig. 2: The Additional Rule of Tableaux Modulo Theory

Fig. 3 :

 3 Fig. 3: The Additional Rule of Polarized Tableaux Modulo Theory

Fig. 4 :

 4 Fig. 4: Proof of a ⊆ a in Deduction Modulo Theory