  The Vehicle Routing Problem (VRP) is the combinatorial optimization problem
of computing routes to serve customers while minimizing a cost function,
typically the travelled distance or the number of vehicles required for a given
performance. Industrial applications of the problem in manufacturing plants is
the scheduling and routing of Automated Guided Vehicles (AGVs) to deliver
material between storage areas and assembly stations. For large fleets of
vehicles it is necessary to take the limited space of plant floor into account
during scheduling and routing in order to limit the number of AGVs that are at
certain locations at a given time. In addition, AGVs are most often powered by
batteries and therefore have limited operating range and non-negligible
charging time that will also affect the scheduling and routing decisions. In
this paper we provide a model formulation for the scheduling and routing of
AGVs with given time-windows for delivering material, restricted by capacity
constraints on the path network, and with the need for periodic recharge. The
problem is modelled and solved using optimizing Satisfiability Modulo Theory
(SMT) solvers. The approach is evaluated on a set of generated problem
instances, showing that the solver can handle medium size instances in a
reasonable amount of time.
