劉錫鵬, 陳 寅

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

1 引言

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

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

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

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

2 研究背景

2.1 機組排班問題概述

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

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

2.2 已有的研究工作

機組排班問題是復雜的組合優(yōu)化問題, 通?？蓪⑵涿枋鰹榧戏指顔栴}(Set Partition Problem, SPP)或集合覆蓋問題(Set Covering Problem, SCP). 本文將已有的研究工作分為確定性算法和非確定性算法.

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

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

2.3 SMT求解技術(shù)介紹

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

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

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

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

3 機組排班模型及算法設(shè)計

3.1 問題的模型

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

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

任務環(huán)成本cp如下所示:

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

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

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

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

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

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

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

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

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

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

3.2 航班任務環(huán)的生成

3.2.1 航班任務環(huán)生成算法

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

算法1. 航班網(wǎng)絡的建立輸入: 航班集合I, 基地集合B, 所有相關(guān)約束C, 從機場出發(fā)的航班集合DepMap輸出: 航班網(wǎng)絡集合1. 初始化SB, EB //航班網(wǎng)絡虛擬節(jié)點 , 分別表示從基地B出發(fā)和結(jié)束2. for SB的每個子集Sb do //b為具體的基地機場3. for i in DepMap[b] do //DepMap[b]表示從基地b出發(fā)的航班集合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所示, 設(shè)虛擬起點為Sb, 對應的終點為Eb, 其中b是基地機場, ?b∈B,B為所有基地機場的集合, 尋找從起點Sb到 終點Eb的航班路線, 最終生成n個航班網(wǎng)絡,n為基地機場的數(shù)量. 首先將所有航班按照起飛機場進行歸類, 目的是在后續(xù)的航班銜接過程中滿足地點銜接約束, 避免在建立航班網(wǎng)絡過程中不必要的路徑搜索, 提高搜索效率. 將每個航班都看作為網(wǎng)絡中的一個節(jié)點, 節(jié)點包含航班的航班號、起飛時間和降落時間、起飛機場和降落機場等信息, 先建立從起點Sb到從基地b出發(fā)的航班節(jié)點的連接路徑, 然后遍歷從Sb到達航班節(jié)點, 對每個航班節(jié)點, 找到該航班的降落機場, 遍歷從該機場出發(fā)的航班集合, 若滿足后一航班的起飛時間和前一航班的降落時間差大于最小連接時間約束, 則建立從前一航班節(jié)點到后一航班節(jié)點的一條路徑, 從當前節(jié)點進行遞歸, 直到某一航班節(jié)點的降落機場為b, 則建立從該航班節(jié)點到終點Eb的路徑. 航班網(wǎng)絡的示意圖如圖1所示.

圖1 航班網(wǎng)絡連接示意圖

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

算法2. 初始航班任務環(huán)生成Sb輸入: 航班網(wǎng)絡 , 約束C輸出: 航班任務環(huán)P P=?//初始化航班任務環(huán)集合1. foriinSb.childrendo 2. Fp=?3. ft,dt=0 //初始化總飛行時間和總執(zhí)勤時間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 初始航班任務環(huán)生成實例

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

表1 某航班計劃表

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

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

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

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

(2)生成航班連接網(wǎng)絡

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

圖2 初始航班網(wǎng)絡

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

圖3 部分航班網(wǎng)絡示意圖

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

根據(jù)上述生成的航班網(wǎng)絡, 利用深度優(yōu)先搜索, 加入約束條件, 如飛行時間、執(zhí)勤時間等, 得到滿足約束條件的航班任務環(huán), 最終生成了14個合法的可行航班任務環(huán), 生成的航班環(huán)如表2所示.

表2 生成的合法航班環(huán)

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

3.2.3 航空公司任務環(huán)生成實例

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

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

圖4 航班連接網(wǎng)絡圖

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

表3 航班任務環(huán)實例

3.3 優(yōu)化求解算法

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

算法3. 基于Z3的增量優(yōu)化求解輸入: 機場的集合AP, 基地集合BS, 航班的集合I(1.. n), 任務環(huán)生成函數(shù)GenPairing(), 參數(shù)level輸出: 最終任務環(huán)FP, 成本costs P=?,costs=0,fts,dts=0,S=Optimize()1. (l=0;l≤level;l++)2. for P*,Cost*=GenPairing(l) //根據(jù)level生成航班任務環(huán)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, 航班任務環(huán)生成函數(shù)GenPairing(), 其中GenPairing()可以輸入的參數(shù)level生成不同層次的任務環(huán), 如level=0時生成當天返回基地的任務環(huán),level=1時生成當天未返回基地的任務環(huán)等.

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

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

表4 優(yōu)化求解后的任務環(huán)

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

4 實驗分析

4.1 實驗環(huán)境及實驗分析

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

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

表7 各組航班環(huán)數(shù)量

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

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

表8 模型求解結(jié)果

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

4.2 實驗對比

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

經(jīng)過實驗, 得出實驗結(jié)果如表9所示.

表9 實驗結(jié)果對比

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

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

5 總結(jié)

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

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