Tamkin Khan
M.Sc. Candidate
Supervisor: Dr. Antonina Kolokolova

Glider mission planning using generic solvers

Department of Computer Science
Tuesday, May 13, 2014, 11:00 a.m., Room EN 2022

---

Abstract

"Autonomous underwater vehicles (AUV), in particular gliders, have been used for many tasks such as underwater surveys. Modern-day gliders can perform month-long missions. During a mission, several factors impact their performance: ocean currents, lack of communication and GPS while under water, weather. At present engineers do not seem to do much mission planning, supplying a glider with a list of goals created by hand. Developing techniques for planning such missions for possibly heterogeneous groups of gliders is the goal of this project. 

At the heart of such mission planning problem are variants of the Asymmetric Traveling Salesman problem: as it is NP-hard, there is no known algorithm to solve it exactly in polynomial time. However, over the last decade heuristic solvers, in particular solvers based on Integer Linear Programming and Satisfiability, have been used successfully in practice to solve industrial instances of many NP-hard problems.

In this thesis we developed a glider mission planner based on such solvers. In particular, we used a Mixed Integer Linear Programming (MILP) solver CPLEX, several Pseudo-Boolean Optimization (PBO) solvers Sat4j, Clasp and SCIP and Satisfiability Modulo Theories (SMT) solver Z3 as the core engine of our planner; in addition to different solvers, we considered several different encodings of the problem. In our experiments, Mixed Integer Linear Programming solver has been the most successful.

An important question in satisfiability/heuristic solver research is modelling the real-world instances distribution by a synthetic distribution. Here, we compared the performance of the solvers on instances of ATSP coming from ocean current data with their performance on crafted instance of random graphs, Euclidean graphs and Euclidean with varying amounts of noise, both symmetric and asymmetric."