Mardi 2 Février
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A Tabu Search Heuristic for a Staff Scheduling Problem |
Description: |
Stefania Pan Scheduling problems form a very large class of optimization problems en- countered in several industries and organizations of widely different kinds. The particular problem that we consider is a staff scheduling problem, which con- sists of assigning activities to employees by taking into account workload re- quirements and different other constraints (for instance legal, economic, or- ganizational and social constraints). Staff scheduling problems are NP-hard, heuristics methods are often used to deal with large scale practical problems. We focus on constraints which impose minimum and maximum duration on activities. These constraints make the problem difficult to solve. We propose a Tabu Search (TS) approach to deal with the specific staff scheduling problem taking into account workload requirements and activities duration constraints. Computational results show the effectiveness of the proposed approach compar- ing CPLEX solver. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Generating series of the trace group, and Möbius inversion |
Description: |
Anne Bouillard |
Mardi 9 Février
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Primal Heuristics for Branch-and-Price |
Description: |
Francois Vanderbeck Math heuristics have become an essential component in mixed integer programming (MIP) solvers. Extending generic MIP heuristics, our study outlines generic procedures to build primal solutions in the context of a Branch-and-Price approach and reports on their performance. Rounding the linear relaxation solution of the Dantzig-Wolfe reformu-lation, which is typically tighter than that of the original compact formulation, sometimes produces better solutions than state-of-the-art specialised heuristics as revealed by our numerical experiments. We focus on the so-called diving methods and their combination with diversification-intensification paradigms such as Limited Discrepancy Search, sub-MIPing, relaxation induced neighbourhood search, local branching, and strong branching. The dynamic generation of variables inherent to a column generation approach requires specific adaptation of heuristic paradigms. Our contribution lies in proposing simple strategies to get around these technical issues. Our numerical results on Generalized Assignment, Cutting Stock, and Vertex Coloring problems sets new benchmarks, highlighting the performance of diving heuristics as generic procedures in a column generation context. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
TBC |
Description: |
Nicolas Basset |
Jeudi 11 Février
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Timed Aggregate Graph : a finite graph for model checking of Time Petri Nets |
Description: |
Amal Chamakh Time Petri Nets (TPNs) are one of the most powerful formalisms for the specification and the verification of systems involving explicit timing constraints. To deal with model checking of timed systems modeled by TPNs, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves timed traces and reachable states of the corresponding TPN and allows for on-the-fly verification of reachability properties. We also introduce an algorithm for a modular construction of the TAG, to better confine the state explosion problem. |
Vendredi 12 Février
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Hacking Nondeterminism with Induction and Coinduction |
Description: |
Damien Pous Finite automata are used in a wide range of verification problems. We introduce "bisimulation up to congruence" as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker "bisimulation up to equivalence" technique. The resulting algorithm can be exponentially faster than the recently introduced "antichain algorithms". |
Mardi 16 Février
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
TBC |
Description: |
Benjamin Hellouin |
Jeudi 18 Février
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Sampled Weighted Min-Hashing for Large-Scale Topic Mining |
Description: |
Ivan Vladimir MEZA Sampled Weighted Min-Hashing (SWMH) is a randomized approach to automatically mine topics from large-scale corpora. SWMH generates multiple random partitions of the corpus vocabulary based on term co-occurrence and agglomerates highly overlapping inter-partition cells to produce the mined topics. While alternative approaches define a topic as a probabilistic distribution over the complete vocabulary, SWMH topics are subsets of such vocabulary. Interestingly, the topics mined by SWMH underlie themes from the corpus at different levels of granularity. We extensively evaluate the meaningfulness of the mined topics both qualitatively and quantitatively on the NIPS (1.7K documents), 20 Newsgroup (20K), Reuters (800K) and Wikipedia (4M) corpora. |
Vendredi 19 Février
Heure: |
11:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Relational type-checking of connected proof-structures |
Description: |
Luc Pellissier It is possible to define a typing system for Multiplicative Exponential Linear Logic (MELL): in such a system, typing judgments are of the form ? R : x : ?, where R is a MELL proof-structure, ? is the list of types of the conclusions of R, and x an element of the relational interpretation of ?, meaning that x is an element of the relational interpretation of R (of type ?). As relational semantics can be used to infer execution properties of the proof-structure, these judgment can be considered as forms of quantitative typing. We provide an abstract machine that decides, if R satisfies a geometric condition, whether the judgment ? R : x : ? is valid. Also, the machine halts in bilinear time in the sizes of R and x. |
|
|