Abstract:Crew scheduling is an important part of an airline operation plan. Reasonable crew scheduling can help airlines save great crew costs and increase their revenue. Since the crew scheduling process involves massive complex constraints, it is an NP-hard problem; thus it is difficult to optimize the solution. This study proposes an optimal solution to crew scheduling problems according to Satisfiability Modulo Theories (SMT), which converts various constraints in the crew scheduling process into first-order logic formulas and sets the solution goal as minimum cost and maximum crew utilization. In addition, it transforms the problem into an optimal solution under the satisfiable condition of the given logic formula and uses the SMT solver, Z3. Experiments show that the algorithm in this study can solve the crew scheduling problem of a certain-scale flight plan, bringing benefits to airlines.