الفهرس Only 14 pages are availabe for public view
 |  | from | 126 |  |  |
| | | from | 126 | | |
Abstract
The vehicle routing problem (VRP) is the problem of designing a specific number of routes to serve a given number of customers while achieving optimal total travel distance and optimal number of routes. Additional attributes have been imposed on the problem such as capacity constraints and time window constraints. Vehicle routing problem with time window constraints (VRPTW) restricts that the service time of each customer should start within a time window. These problems are known to be NP-hard. Different approaches have been tried to solve these problems such as heuristic and metaheuristic approaches. In this thesis we propose to transform the NP-hard problem into another. Our approach is based on satisfiability modulo theories (SMT). Using SMT poses transformability challenges in order to take advantage of its relative time competitiveness. We successfully apply SMT to solve VRPTW. Our solution proves to be competitive to other optimization techniques while it significantly decreases the solution time opening the door to solve much larger problems. In addition, it sets proof for using SMT for solving optimization problems