基于SMT的机组排班问题优化求解  

Optimal Solution to Crew Scheduling Problem Based on SMT

作　　者：刘锡鹏 陈寅[1] LIU Xi-Peng;CHEN Yin(School of Computer,South China Normal University,Guangzhou 510631,China)

机构地区：[1]华南师范大学计算机学院,广州510631

出　　处：《计算机系统应用》2021年第12期279-287,共9页Computer Systems & Applications

摘　　要：机组排班是航空公司运营计划非常重要的一个环节,合理的机组排班可以为航空公司省下一大笔机组成本支出,从而增加航空公司的收益.由于机组排班过程涉及大量的复杂约束,属于NP难问题,因此优化求解困难.本文提出了一种基于可满足性模理论(Satisfiability Modulo Theories,SMT)的航空公司机组排班问题的优化求解方法,将机组排班过程中的各种约束转化为一阶逻辑公式,设立求解目标为最小化成本和最大化机组利用率,将问题转化为求在给定逻辑公式可满足情况下的最优解,并利用SMT求解器Z3进行求解.实验表明,本文的算法能有效的求解一定规模航班计划的机组排班问题,给航空公司带来一定的收益.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.

关 键 词：可满足性模理论(SMT) 一阶逻辑 机组排班 优化模型 Z3 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程] V35[自动化与计算机技术—控制科学与工程]