Hybrid of Hill Climbing and SAT Solving for Air Traffic Controller Shift Scheduling

Abstract

Modern computers solve many problems by using exact methods, heuristic methods and very often by using their combination. Air Traffic Controller Shift Scheduling Problem has been successfully solved by using SAT technology (reduction to logical formulas) and several models of the problem exist. We present a technique for solving this problem that is a combination of SAT solving and meta-heuristic method hill climbing, and consists of three phases. First, SAT solver is used to generate feasible solution. Then, the hill climbing is used to improve this solution, in terms of number of satisfied wishes of controllers. Finally, SAT solving is used to further improve the found solution by fixing some parts of the solution. Three phases are repeated until optimal solution is found. Usage of exact method (SAT solving) guarantees that the found solution is optimal; usage of meta-heuristic (hill climbing) increases the efficiency in finding good solutions. By using these essentially different ways of solving, we aim to use the best from both worlds. Results indicate that this hybrid technique outperforms previously most efficient developed techniques.