基于SMT的機組排班問題優化求解①

劉錫鵬, 陳 寅

(華南師范大學 計算機學院, 廣州 510631)

1 引言

航空公司運營計劃包括航班計劃、飛機排班計劃和機組排班計劃等, 其中機組排班計劃是運營計劃的重要組成部分. 近年來隨著民航業的發展, 航線網絡日益復雜, 民航管理局等相關部門為保障飛行安全制定了相關的行業規范, 例如CCAR-121-R6[1]等. 由于航線和約束的復雜性, 單純使用手工模式進行排班是十分困難的, 另一方面, 航班計劃在執行過程中難免會遇到由機械故障、天氣原因或者機場調度等原因造成的航班變更, 因此在已有計劃的基礎上靈活地調整航班安排也是一個非?，F實的需求. 由于人力成本的上升, 機組人員的收入水平提高, 機組排班的結果直接決定航空公司的實際機組成本支出, 從而影響航空公司的運營收益. 因此, 在滿足相關約束下保障飛行安全的同時設計一個良好高效的算法來完成機組排班計劃的編排對于航空公司提高運營效率和增加收益有著重要的現實意義.

本文提出一種基于可滿足性模理論(Satisfiability Modulo Theories, SMT)的機組排班問題的優化求解方式. SMT在布爾可滿足性理論(SAT)的基礎上加入背景理論(例如, 算術運算、向量和數組等), 可以適用于更廣泛的應用場景. 機組排班問題中既存在一些邏輯約束, 又存在一些數量約束, 因此考慮采用SMT來進行求解. 另一方面, 現代的SMT求解器都支持增量式的求解(incremental solving), 即可在求解的任何階段, 增加或者刪除約束, 而無需重新搜索整個狀態空間,這也為航班排班中靈活調整的實現帶來的便利.

本文通過對機組排班問題的分析, 建立了機組排班問題的多目標優化模型, 將各種約束表述為一階邏輯公式, 并利用SMT求解器Z3進行增量求解, 實現了一定規模的機組排班問題的優化求解.

本論文的組織結構如下: 在第2節, 對機組排班問題的定義、已有的研究工作以及SMT求解技術進行詳細介紹. 在第3節, 提出機組排班的數學模型和相應算法. 在第4節, 通過實驗對航班實例進行求解并對結果進行分析. 在第5節也是最后一節, 對全文的工作做出系統性的總結.

2 研究背景

2.1 機組排班問題概述

機組排班計劃問題是指在民航管理局相關適航文件和具體航空公司制定的一系列規定的前提下, 將航班計劃內的各個航班合理的分配給機組飛行員和乘務人員執行的過程. 在航空公司運營總成本中, 機組成本是僅次于燃料成本的第二大費用[2], 由于機組成本比燃料成本具有更好的可控性, 通過合理的分配可降低一些不必要的額外成本, 為航空公司帶來更多的收益. 為了保障飛行安全, 機組排班過程往往涉及大量的約束,要滿足一系列相關法律法規對飛行時間、人員要求等嚴格規定, 這使得機組排班模型復雜, 優化求解困難,屬于NP難問題[3].

機組排班計劃問題一般分為兩個子問題: 機組排班問題和機組人員指派問題. 其中機組排班問題又稱為機組配對問題, 其任務是在滿足相關約束條件下生成一系列可由機組執行的從機組基地出發并最終返回基地的航班任務環, 要求覆蓋所有待執行的航班, 優化目標是任務環成本的最小化[4]. 機組人員指派問題[5]的任務是要將機組排班階段生成的任務環中的任務合理的分配給具體的機組人員執行, 要求考慮任務分配的公平性原則. 本文主要研究機組排班問題.

2.2 已有的研究工作

機組排班問題是復雜的組合優化問題, 通常可將其描述為集合分割問題(Set Partition Problem, SPP)或集合覆蓋問題(Set Covering Problem, SCP). 本文將已有的研究工作分為確定性算法和非確定性算法.

非確定性算法方面, Kornilakis等[6]采用啟發式兩階段求解方法, 先利用深度優先算法尋找所有可行任務環, 然后從所有任務環中選擇最小成本的任務環組合, 選擇了遺傳算法來進行航班的組合優化. 趙天洋[7]對機組排班理論和算法進行分析, 比較了常用的遺傳算法、蟻群算法和模擬退火算法的優缺點, 對機組排班各階段進行分析設計, 將機組排班過程分為勤務生成、機組排班優化和機組人員指派3個部分, 采用改進的遺傳算法進行優化求解. 吳蘇陽[8]考慮機組排班中任務環組環的質量和效率, 從航空公司運營成本、生產計劃的穩定性、生產計劃質量和飛行時間均衡方面對飛行任務的組環進行優化, 采用遺傳算法求解.Aggarwal等[9]提出了一種用于大規模復雜航班網絡生成初始航班任務環的啟發式算法, 采用分割和覆蓋方法, 從大規模航班數據中隨機分割部分航班生成任務環, 然后將優化求解后的任務環加入初始航班任務環(IFS)中, 直到所有航班被覆蓋. 張文成等[10]提出改進二進制粒子群算法用于機組配對優化, 以機組利用率最大為優化目標, 利用深度優先搜索算法從航班計劃表中生成初始航班配對, 在改進二進制粒子群算法尋優過程中引入懲罰因子和自適應權重, 提高了算法的速度和解的質量. Chen等[11]整合飛機排班和機組排班問題, 提出多目標組合優化模型, 采用NSGA-II(帶精英策略的非支配排序的遺傳算法)結合修復策略求解, 通過實際數據實驗得出的時刻表比專家制定計劃更優.

在確定性算法方面, Marsten等[12]建立了機組排班問題的集合分割模型, 采用拉格朗日松弛和次梯度優化方法進行求解. Graves等[13]采用列生成算法對機組排班問題進行求解, 系統分為生成器和優化器, 生成器負責生成候選航班配對傳遞給優化器, 優化器負責尋找使總成本最小的一組航班配對, 通過不斷迭代至最優并覆蓋所有航班. 藍伯雄等[14]在機組排班階段采用混合集合規劃進行高層建模, 利用一階邏輯和集合推理對機組排班問題進行表述, 將運籌學優化方法與業務邏輯相結合, 建立了貼近實際的機組排班模型.Zeighami等[15]集成了機組排班問題和機組人員分配問題, 綜合考慮機組成本和飛行員喜好, 提出結合拉格朗日分解、列生成法和動態約束聚合的綜合算法,實驗表明該方法能有效節省大量成本和滿足機組人員喜好.

2.3 SMT求解技術介紹

可滿足性模理論(Satisfiability Modulo Theories,SMT)[16]是指檢查給定的在相關背景理論(如算術、位向量、數組和未解釋函數等)下一階邏輯公式是否可滿足的問題. 給定一個SMT公式F, 如果存在一組賦值使得F為真, 則稱F是可滿足的, 否則稱F是不可滿足的. SMT是一種說明性語言, 可以使用一階邏輯語言描述問題的約束, 同時支持各種復雜約束, 能很好的描述NP及co-NP問題, 在優化問題求解[17]、程序驗證[18]、靜態分析[19]等領域有突出優勢.

SMT的判定方法一般被稱為SMT求解器(SMT solver), 目前主流的SMT求解器有Z3[20]、CVC4、Yices2等, 這些求解器都能較好的處理大規模工業化問題, 本文采用的是微軟的Z3作為SMT求解器來求解機組排班問題.

Z3是微軟組織開發的SMT求解器, 在擴展性、表達能力以及求解效率等方面都較為出色, 是目前最好用的SMT求解器之一. Z3在Github發布了開源的項目, 在近年來的SMT求解器的競賽中一直處于領先的地位. Z3內部采用一種類似于Lisp的SMT-LIBv2語言[21], 同時也提供了包括C, C++和Python等常用的編程語言接口. 本文采用的Z3Py就是Z3提供的Python開發包, 可以方便約束求解和系統其它部分的接口.Z3支持多種理論, 不僅可以用于驗證多個邏輯公式的可滿足性, 也能給出一組滿足約束的解； 此外還支持增量求解, 可以在不改變原問題基礎上增加新的約束, 而無需重新計算, 加快了求解速度. Z3采用棧的方式, 可以在新約束不滿足時回退到上一個階段.

機組排班問題本質上是在一系列約束條件下的優化求解問題, 要滿足民航局和航空公司制定的關于飛行安全的復雜適航條例, 屬于NP難問題. SMT可以通過一階邏輯公式很好的表達機組排班過程中各種復雜的約束, 在優化求解方面具有突出優勢, SMT求解器Z3在擴展性、表達能力以及求解效率等方面都較為出色, 通過設置求解目標, 可以在滿足相關約束的情況下高效地求解出問題的最優解.

3 機組排班模型及算法設計

3.1 問題的模型

機組排班問題中機組排班問題通常用集合分割模型表示, 本文以最小化任務環總成本為主優化目標, 以最大化機組利用率為次目標建立多目標優化模型. 其中機組成本包括任務津貼、飛行津貼、在外過夜成本以及加機組成本等, 任務津貼是機組執行任務所要支付的必要成本； 飛行津貼是機組參與飛行時的補貼, 一般與飛行時間有關； 過夜成本是指機組在執行的某一天的任務中, 最后的航班降落機場為非基地機場, 無法回到基地休息而在外過夜產生的旅店成本； 加機組成本是一個機組為了完成某個任務而作為乘客搭乘另一個機組的航班到達目的地執行任務而產生的額外開支.機組利用率是機組執行任務中有效的工作時間占據的比重, 等于機組飛行時間/機組執勤時間.

假設P是所有航班任務環的集合,p是P中一個任務環,cp是 任務環p的總成本,xp是0-1變量, 表示任務環是否被選中為最終的任務環, 則主目標函數Obj1如下:

任務環成本cp如下所示:

其中,cduty表 示任務津貼,cf是每小時的飛行津貼,fti為航班的飛行小時數,covernight為過夜成本,csit表示加機組成本.

第二目標是最大化機組利用率, 假設I是所有待執行的航班集合,i是其中某個航班, ?i∈I, 設fti為航班i的飛行時間,dti為 航班i的執勤時間,Fp,t為任務環p在第t天的航班集合, 則第二目標函數Obj2如下:

假設aip是0-1變量,表示航班i是否在任務環p中,depi表示航班i的起飛機場,arri是航班i的降落機場,tdepi是航班i的起飛時間,tarri是航班i的降落時間,minct表示最小間隔時間,maxfts表示機組每天的最大飛行時間,maxdts是機組每天的最大的執勤時間,j航班是i航班的后續航班, 則要滿足的基本約束條件有:

其中, 式(3)是航班覆蓋約束, 即每個航班有且僅有一次出現在選中航班任務環中.

式(4)是航班地點銜接約束, 要求后一個航班的起飛機場要與前一個航班的降落機場一致.

式(5)是航班過站時間約束, 要求后一個航班的出發時間與前一個航班的降落時間之差要大于最小航班連接時間限制.

式(6)為飛行時間約束, 要求在每一天機組總飛行時間不能超過最大飛行時間限制.

式(7)為執勤時間約束, 要求在每一天機組總執勤時間不能超過最大執勤時間限制.

式(8)為航班任務環總跨度約束, 即每個任務環的日期跨度不能超過最長時間跨度約束, date表示當前航班的日期.

式(9)中,aip,xp是0-1變量,FP,Fp,t是集合變量,是所有航班集合I的子集.

3.2 航班任務環的生成

3.2.1 航班任務環生成算法

初始航班任務環生成階段分成兩步, 首先利用航班信息和相關約束通過改進的深度優先算法建立航班網絡, 然后再利用DFS遍歷所有航班網絡生成初始航班任務環[22]. 航班網絡的建立過程如算法1所示.

算法1. 航班網絡的建立輸入: 航班集合I, 基地集合B, 所有相關約束C, 從機場出發的航班集合DepMap輸出: 航班網絡集合1. 初始化SB, EB //航班網絡虛擬節點 , 分別表示從基地B出發和結束2. for SB的每個子集Sb do //b為具體的基地機場3. for i in DepMap[b] do //DepMap[b]表示從基地b出發的航班集合4. add childNode i to Sb 5. for j in DepMap[iarr] do(i→j)6. if 滿足約束 C then 7. add childNode j to i 8. if jarr=b；9. add childNode Eb to j 10. return 11. else DFS(j,DepMap,C)12.

如算法1所示, 設虛擬起點為Sb, 對應的終點為Eb, 其中b是基地機場, ?b∈B,B為所有基地機場的集合, 尋找從起點Sb到 終點Eb的航班路線, 最終生成n個航班網絡,n為基地機場的數量. 首先將所有航班按照起飛機場進行歸類, 目的是在后續的航班銜接過程中滿足地點銜接約束, 避免在建立航班網絡過程中不必要的路徑搜索, 提高搜索效率. 將每個航班都看作為網絡中的一個節點, 節點包含航班的航班號、起飛時間和降落時間、起飛機場和降落機場等信息, 先建立從起點Sb到從基地b出發的航班節點的連接路徑, 然后遍歷從Sb到達航班節點, 對每個航班節點, 找到該航班的降落機場, 遍歷從該機場出發的航班集合, 若滿足后一航班的起飛時間和前一航班的降落時間差大于最小連接時間約束, 則建立從前一航班節點到后一航班節點的一條路徑, 從當前節點進行遞歸, 直到某一航班節點的降落機場為b, 則建立從該航班節點到終點Eb的路徑. 航班網絡的示意圖如圖1所示.

圖1 航班網絡連接示意圖

航班網絡建立完成后, 初始航班環生成如算法2所示. 對于 ?b∈B, 利用深度優先算法遍歷從Sb到Eb的航班路徑, 在遍歷過程中統計路徑中航班的飛行時間和執勤時間, 若到達某一航班節點時飛行時間或執勤時間已經超過了相關規定中對于飛行時間和執勤時間限制時, 不繼續遞歸, 進行回溯, 回到上一個節點繼續遍歷, 直到滿足約束的所有的路徑都被遍歷完, 則每一條可行路徑都是一個合法的可行任務環, 此時初始航班任務環生成完成.

算法2. 初始航班任務環生成Sb輸入: 航班網絡 , 約束C輸出: 航班任務環P P=?//初始化航班任務環集合1. foriinSb.childrendo 2. Fp=?3. ft,dt=0 //初始化總飛行時間和總執勤時間4. additoFp 5. ifi.childrennotnullandft,dt滿足約束C：6. ft=ft+ift,dt=dt+idt 7. forjini.childrendo 8. DFS(j,Fp)9. else 10. addFptoP 11. Fpremovelast 12.

3.2.2 初始航班任務環生成實例

下面通過舉例來說明航班任務環的生成, 給定一組航班計劃表, 如表1所示, 其中包括18個航班, 每個航班包括航班號、執飛機型、起飛/降落機場, 起飛/到達時間等信息, 該航班計劃中有6個機場, 其中廣州為基地機場, 其余為非基地機場.

表1 某航班計劃表

首先生成航班連接網絡, 再根據航班網絡進行深度優先搜索尋找滿足約束的航班任務環. 假設該航班計劃表的基本約束條件如下: 機組每天的總飛行時間不超過8小時, 機組每天總執勤時間不超過14小時,航班銜接時間不少于30分鐘, 任務環每天的航班數不超過4個. 則生成初始可行航班任務環的步驟如下；

(1)按起飛機場對航班進行歸類

該航班計劃共有6個機場, 分別為廣州、南昌、杭州、貴陽、桂林、長沙, 按起飛機場來劃分可分為如下組合:

廣州(0, 5, 7, 9, 11, 16)； 南昌(1, 6, 8, 10)； 貴陽(2,3, 17)； 杭州(4, 14)； 桂林(12)； 長沙(13, 15)

(2)生成航班連接網絡

由于任務環都是從基地出發, 且該航班計劃只有廣州一個基地機場, 因此建立虛擬起始節點到所有從廣州出發航班節點的連接, 如圖2所示.

圖2 初始航班網絡

然后在初始網絡的基礎上, 遍歷每一個節點對每個節點, 尋找與其降落機場對應的航班集合, 如0號航班的降落機場為南昌, 則對起飛機場為南昌的集合進行遍歷, 驗證其是否滿足航班銜接約束, 若不滿足則舍棄, 若滿足則建立連接, 將其加入航班網絡中, 以此類推, 直到當前節點的到達機場為基地機場廣州為止, 然后將終止節點與虛擬終止節點Eb, 航班網絡建立完成.由于涉及的路徑較為復雜, 圖3僅以從0號航班開始為例, 構建部分航班網絡示意圖.

圖3 部分航班網絡示意圖

(3)搜索可行航班任務環

根據上述生成的航班網絡, 利用深度優先搜索, 加入約束條件, 如飛行時間、執勤時間等, 得到滿足約束條件的航班任務環, 最終生成了14個合法的可行航班任務環, 生成的航班環如表2所示.

表2 生成的合法航班環

由表2可知, 生成的任務環的飛行時間和執勤時間均滿足相應約束, 而并非所有航班環的機組利用率都是高效的, 機組利用率低導致機組在任務過程中空閑時間太長, 不能很好地體現機組的飛行價值, 而機組利用率也是優化求解的目標之一.

3.2.3 航空公司任務環生成實例

為了驗證任務環生成算法的有效性, 本節采用國內某航空公司一周航班計劃的真實數據(對航班號進行了隱藏, 部分起飛和降落機場有所調整), 該航班計劃共有7天, 共有576個航班, 每天的航班數量為80個左右, 主要基地機場為廣州, 次基地有貴陽、三亞等, 根據航班網絡生成算法建立航班連接網絡, 由于頁面限制, 圖4僅展示第一天從廣州基地出發的一個航班連接網絡(省略了首尾的虛擬節點).

圖4中每個節點代表一個航班, 節點內為航班的虛擬編號, 為方便展示, 在節點左右兩邊分別標注了該航班的起飛機場和降落機場.

圖4 航班連接網絡圖

航班網絡生成后, 利用航班環生成算法生成了高質量的航班任務環2303個, 部分航班環實例如表3所示, 其中日期表示任務環中跨越的日期, 時間單位h和min表示小時和分鐘.

表3 航班任務環實例

3.3 優化求解算法

初始航班任務環生成后, 利用SMT求解器Z3對模型進行表述, 假設輸入航班集合為I, 初始航班任務環集合為IP, 定義Z3求解器模式為Optimize, 定義不解釋函數PC(p)表示任務環p是否被選中, 函數的結果為Bool變量(true和false), 則基于Z3的增量求解的過程如算法3所示.

算法3. 基于Z3的增量優化求解輸入: 機場的集合AP, 基地集合BS, 航班的集合I(1.. n), 任務環生成函數GenPairing(), 參數level輸出: 最終任務環FP, 成本costs P=?,costs=0,fts,dts=0,S=Optimize()1. (l=0;l≤level;l++)2. for P*,Cost*=GenPairing(l) //根據level生成航班任務環3. Cst=?4. iinI.length 5. for do P1,P2,···,Pk?P*∨P且包含航班i 6. S.add_constain(Ci,l→PC(P1)∨PC(P2)∨···∨PC(Pk))7. Cst.add(Ci,1∧Ci,2∧···∧Ci,l)8. pinP*∨P,Pj≠Pi且Pi∧Pj≠?9. for do S.add_constain(?PC(Pi)∨?PC(Pj))10. pinP*,eachcostinCost*11. for each do costsaddIF(PC(p),cost,0)12. ftsaddIF(PC(p),ft,0)13. dtsaddIF(PC(p),dt,0)14. ut=fts/dts 15. S.minimize(costs),S.maxmize(ut)16. S.push(Cst)//使約束生效17. Wait_for(costs,ut=Check(S))18. unsat:19. if S.pop()20. S.add_constrain(?Cst)//使約束失效21. P=P∨P*22. 23. else if TimeOut 24. return -1 25. else costs,ut,PC 26. return

如算法3所示, 輸入的信息包括航班信息I, 航班任務環生成函數GenPairing(), 其中GenPairing()可以輸入的參數level生成不同層次的任務環, 如level=0時生成當天返回基地的任務環,level=1時生成當天未返回基地的任務環等.

算法遍歷level依次生成不同層次的任務環,5-7行是航班覆蓋約束, 要求每個航班至少被1個任務環覆蓋,Ci,1為控制約束變量, 決定覆蓋約束是否生效.9-10行是唯一性約束, 即任意兩個任務環Pi和Pj不能同時包含同一個航班. 11-14行利用Z3的IF函數, 將滿足PC(p)=true的任務環p的飛行時間ft、執勤時間dt、成本cost增加到總時間fts和dts和成本costs中.17-26行利用Z3的增量求解技術,先將控制變量Cst對應的約束生效, 利用求解器S進行Check()求解,若超過規定時間則返回-1, 若求解器S返回結果為unsat時, 則進行回溯, 使控制的約束失效, 更新任務環P, 并進入下一輪循環； 當求解器S在給定的時間內給出sat結果時, 返回優化求解后的最終任務環以及總成本costs和機組利用率ut.

下面仍以表1的航班計劃表為例, 闡述優化求解的過程. 航班總數為18, 經過GenPairing(0)生成了第一階段當天返回基地的初始航班任務環數量為16, 然后對其增加相應的約束進行Check()檢查, 發現結果為unsat, 使部分約束失效后進行下一階段GenPairing(1)生成當天未返回基地的不完全任務環11-17、0-10等,由于未返回基地增加過夜成本, 加入先前的任務環中, 添加相應約束進行求解, 仍為unsat, 再下一階段GenPairing(2)增加覆蓋次數較少的航班2、7、10等加入任務環后, 結果為sat, 最終生成的任務環如表4所示.

表4 優化求解后的任務環

由最后的結果可知, 生成的任務環覆蓋了所有的航班, 且每個航班有且僅被覆蓋一次, 同時, 總成本也較低, 機組利用率超過了0. 6, 說明該方法是有效的.

4 實驗分析

4.1 實驗環境及實驗分析

本文對航空公司機組排班問題進行優化求解, 實驗環境選擇個人電腦, CPU為AMD Ryzen5 1600X 6核心12線程, 內存16 GB, Win10系統, 編程語言選擇Python, SMT求解器選擇Python版本的Z3Py[23], 實驗數據來自Kasirzadeh等[24]提供的航空公司的一組航班計劃數據. 本文選取前7天航班計劃數據來驗證求解結果和性能, 按照跨越天數將其分為7組, 數據的基本信息如表5所示, 部分航班時刻表如表6所示.

表6中, 表頭leg_nb表示航班編號, airport_dep與airport_arr分別表示航班的出發機場和到達機場,date_dep、hour_dep表示航班出發的日期和時間,date_arr、hour_arr表示航班到達日期和到達時間.表中, BASE*表示該機場為基地機場, AIR*表示機場為非基地機場. 經過改進的航班網絡生成和DFS算法, 有效的減少了生成的初始航班任務環的數量,按照不同的level參數, 生成用于求解的航班環數量如表7所示.

表7 各組航班環數量

優化求解階段, 利用Z3的增量求解機制, 依次對不同level生成的任務環進行check檢查其是否滿足相應約束, 直到結果為sat, 進行優化求解. 實驗表明, 當level=2時各組數據生成的任務環均可滿足相應的約束.

假設機組每天最大飛行時間為8小時, 最大執勤時間為14小時, 最小銜接時間為30分鐘, 任務津貼為1000, 每小時飛行津貼為400, 過夜成本為500, 加機組成本為500, 機組在任務開始前45分鐘報到, 任務結束后30分鐘完成執勤, 優化求解后生成最終的航班任務環及機組利用率等結果如表8所示.

表8 模型求解結果

從求解結果可知, 該算法能有效的從給定的航班計劃中選擇符合各項約束的任務環. 經過驗證, 生成的任務環能覆蓋所有航班, 且機組利用率均超過了55%,有效的減少了機組的空閑等待時間, 有效的縮短了機組執勤時間, 同時最小化的成本可為航空公司減少一定的機組成本支出, 增加航空公司的收益.

4.2 實驗對比

為了驗證實驗算法的性能, 本文與Agustín等[25]提出的基于偏向隨機化的多起點元啟發式算法以及人工編排方案進行比較分析, 實驗數據來自某小型航空公司的真實案例, 數據來源于文獻[25]. 共有41個航班, 跨越5天, 航班的最小連接時間為45 min, 只有一個基地機場Madrid (MAD).

經過實驗, 得出實驗結果如表9所示.

表9 實驗結果對比

從實驗結果可知, SMT、M-BR與人工編排相比生成的任務環數量更少, 飛行時間更短, 機組成本更低,這是由于人工編排產生了許多不必要的加機組航班,增加了飛行時間和機組成本； SMT相比于M-BR, 機組的利用率更高且求解時間更短.

通過分析實驗結果, 本文提出的SMT算法相較于人工和M-BR算法, 求解效率更高, 總值勤時間更少,機組利用率更高, 更符合航空公司機組排班階段對任務環質量的要求, 可以有效的減少機組成本和提高機組利用率.

5 總結

本文采用基于SMT的研究方法, 對航空公司運營計劃中機組排班計劃問題的機組排班問題進行了研究,綜合考慮了民航管理局等制定的關于飛行安全、人員要求等多種約束, 建立了基于SMT的機組排班優化模型, 采用改進的深度優先搜索算法生成初始航班任務環, 并利用SMT求解器Z3進行模型的優化求解, 并使用增量求解. 實驗表明, 改進的DFS算法能更快速的生成更少更優質的初始航班任務環, 基于SMT的Z3求解器可以更好的表述約束和求解約束, 并可以增量求解, 最終生成機組利用率高且質量較好的航班任務環, 幫助航空公司制定更好的排班計劃以及節約機組成本, 增加收益.

在之后的研究中, 可對機組排班的下一個階段機組人員分配問題進行研究, 制定完整的機組排班計劃,以及在考慮延誤等突發情況下如何增加機組排班的魯棒性進行進一步的研究, 更貼近實際, 減少航班延誤造成的損失.