A new constraint programming model and a linear programming-based adaptive large neighborhood search for the vehicle routing problem with synchronization constraints Minh Ho ang H a*, Tat Dat Nguyen ORLab, VNU University of Engineering and Technology, Hanoi, Vietnam Thinh Nguyen Duy, Hoang Giang Pham, Thuy Do Department of Computer Science and Operations Research, Universit e de Montr eal and CIRRELT, Montr eal, Qu ebec, Canada Louis-Martin Rousseau Ecole Polytechnique de Montr eal and CIRRELT, Montr eal, Canada Abstract. We consider a vehicle routing problem which seeks to minimize cost subject to time window and synchronization constraints. In this problem, the fleet of vehicles is categorized into regular and special vehicles. Some customers require both vehicles' services, whose starting service times at the customer are synchronized. Despite its important real-world application, this problem has rarely been studied in the literature. To solve the problem, we propose a Constraint Programming (CP) model and an Adaptive Large Neighborhood Search (ALNS) in which the design of insertion operators is based on solving linear programming (LP) models to check the insertion feasibility. A number of acceleration techniques is also proposed to significantly reduce the computational time. The computational experiments show that our new CP model finds better solutions than an existing CP-based ANLS, when used on small instances with 25 customers and with a much shorter running time. Our LPbased ALNS dominates the cp-ALNS, in terms of solution quality, when it provides solutions with better objective values, on average, for all instance classes. This demonstrates the advantage of using linear programming instead of constraint programming when dealing with a variant of vehicle routing problems with relatively tight constraints, which is often considered to be more favorable for CP-based methods. Vehicle routing problem, time window, synchronization constraint, constraint programming, adaptive large neighborhood search. 1 Introduction Most of the requirements related to our daily routines are made by a service provider coming to our premises. These types of services can be home care delivery, maintenance operations, public utilities, etc.

Task allocation is ubiquitous in computer science and robotics, yet some problems have received limited attention in the computer science and AI community. Specifically, we will focus on multi-robot task allocation problems when tasks have time windows or ordering constraints. We will outline the main lines ofresearch and open problems.

Hybrid automata networks (HAN) are a powerful formalism to model complex embedded systems. In this paper, we survey the recent advances in the application of Satisfiability Modulo Theories (SMT) to the analysis of HAN. SMT can be seen as an extended form of Boolean satisfiability (SAT), where literals are interpreted with respect to a background theory (e.g. linear arithmetic). HAN can be symbolically represented by means of SMT formulae, and analyzed by generalizing to the case of SMT the traditional model checking algorithms based on SAT.