基于可滿足性模理論的虛擬網映射問題求解

余建軍 吳春明

1(衢州職業技術學院信息工程學院 浙江 衢州 324000) 2(浙江大學計算機科學與技術學院 浙江 杭州310027)

0 引 言

網絡虛擬化技術作為解決互聯網僵化問題的關鍵技術，正成為云計算范式的核心技術。虛擬網映射[1]是網絡虛擬化技術的核心問題，其任務是當單個虛擬網絡構建請求動態到達后，構建該虛擬網絡的映射方案并完成映射。單個虛擬網映射問題是NP難問題[2-3]，求解該問題的精確算法具有非多項式時間復雜度，故當前提出的單個虛擬網映射算法主要集中在啟發式算法[2,4-7]，當然也有少數單個虛擬網映射問題的精確算法被提出，因為精確算法設計對啟發式算法設計具有啟發意義，且精確算法可用于中小規模問題求解以及啟發式算法的性能評估。精確算法可以分為兩階段映射精確算法和一階段映射精確算法兩類[8]。

兩階段映射精確算法采用迭代技術，每次迭代都是在完成虛擬節點映射后進行虛擬鏈路映射，迭代的依據是虛擬網映射方案的目標函數。文獻[9]以映射代價最小化為目標，建立了基于路徑的單個虛擬網映射問題的混合整數規劃模型P-VNE；在分析P-VNE模型的對偶規劃模型的基礎上，提出了求解單個虛擬網映射問題最優解的嵌入于分支限界搜索框架下的列生成算法。文獻[10]以最小化物理網絡資源消耗為目標，通過增強文獻[9]的P-VNE模型，建立了基于路徑的單個虛擬網映射問題的混合整數規劃模型，并基于該模型設計了兩階段映射精確算法。該算法的主要流程如下：① 首先假設部分物理節點已經被虛擬節點所映射；② 基于虛擬網絡拓撲結構進行虛擬鏈路映射，從而形成MILP模型新的約束條件，并得到該虛擬網映射問題的上屆；③ 假設虛擬鏈路已經完成映射，然后完成虛擬節點映射，從而形成MILP模型新的約束條件，并得到該虛擬網映射問題的下屆；④ 重復步驟①、②和③，直到虛擬網映射問題的下屆等于或接近等于上屆。

一階段映射精確算法是指虛擬節點映射和虛擬鏈路映射同時進行的精確算法。一階段映射精確算法是通過建立單個虛擬網映射問題的數學規劃模型，然后通過分枝定界法、整數規劃算法等常用方法求解。文獻[11]以最小化物理網絡資源消耗和負載均衡為目標，建立了基于節點-鏈路的單個虛擬網映射問題的整數線性規劃模型，并采用優化軟件CPLEX求解該模型，該模型的約束條件包括了鏈路延遲約束和虛擬節點最大距離約束。文獻[12]針對小規模的單個虛擬網映射問題，以映射代價最小化為目標建立數學規劃模型，并用優化軟件LINGO來求解。

虛擬網映射問題精確算法設計的關鍵是提高其求解效率，目前所提出的一階段映射精確算法是基于求解數學規劃模型的優化軟件來實現的，其求解效率有待進一步提高，以進一步增強其實用性。鑒于可滿足性模理論在線性邏輯約束公式優化問題求解領域有突出優勢[13]，本文基于可滿足性模理論，設計了虛擬網映射問題一階段映射精確算法，并通過實驗對比和分析，驗證本文方法的有效性。具體而言，針對物理網絡不支持路徑分割且物理節點不支持重復映射的虛擬網映射問題[2]，首先建立以物理網絡資源消耗量最小化為目標的單個虛擬網映射問題的整數線性規劃模型；然后，基于可滿足性模理論[13]提出了一種解決物理網絡不支持路徑分割且物理節點不支持重復映射的虛擬網映射問題的精確求解方法。

1 問題描述和數學模型

1.1 問題描述

1.2 虛擬網映射收益及目標

虛擬網映射問題是在線優化問題，其求解目標往往是多樣化的[2]，如從物理網絡提供商的角度，其目標是最大化長期收益；從服務提供商的角度，其目標是最小化從物理網絡提供商租用的資源量；其他還有節能、安全、容錯等[14]，本文以最大化物理網絡提供商長期收益為其映射目標。在單個虛擬網映射時，因其收益是常數，為達到長期映射目標，最小化映射成本是單個虛擬網映射問題的主要目標[2]，本文將物理網絡資源(CPU容量和物理鏈路帶寬)消耗量定義為映射成本[10,12]。

1.3 整數線性規劃模型

(1)

(3) 約束條件為：

(2)

(3)

(4)

(5)

(6)

式中：si和ti是第i條虛擬鏈路的兩個端點對應的源節點，式(4)、式(5)和式(6)表示流守恒，即除了源節點si和目標節點ti外其他節點的網絡凈流量為0。

(7)

(8)

(9)

式(9)確保每個物理節點最多只能被一個虛擬節點所映射。

2 基于可滿足性模理論求解器的虛擬網映射問題求解

2.1 虛擬網映射問題的SMT公式

命題邏輯可滿足性問題(SATISFIABILITY，SAT)[13]是NPC問題，SAT技術被廣泛應用于自動電子設計、靜態程序分析、測試用例生成等領域。針對SAT存在只面向命題邏輯公式、表達能力有限等問題，人們將SAT擴展為可滿足性模理論(satisfiability module theories，SMT)[13]。SMT是判定一階邏輯公式在組合背景理論下的可滿足性問題，SMT技術在測試用例自動生成、線性邏輯約束公式優化問題求解等領域有突出優勢。

通過構建虛擬網映射問題的SMT公式VNM_SMT，從而將虛擬網映射問題建模為線性邏輯約束求解優化問題。虛擬網映射問題的SMT公式由式(10)-式(19)組成。

(10)

(11)

(12)

(13)

(14)

(15)

(16)

(17)

(18)

蘊涵詞用?表示，A?B等價于A∨B。式(10)確保物理節點剩余CPU容量大于等于映射到該物理節點的虛擬節點的CPU容量需求。式(11)確保任意物理鏈路上所映射的所有虛擬鏈路帶寬之和小于等于該物理鏈路的剩余帶寬。式(12)確保源節點不能成為流的中間節點。式(13)、式(14)和式(15)表示流守恒，除了si對應的源節點和ti對應的目標節點外其他節點的網絡凈流量為0。式(16)確保每個源節點(對應虛擬節點)只能映射到唯一的一個物理節點上。式(17)確保每個物理節點最多只能被一個虛擬節點所映射。式(18)表示優化目標是最小化物理鏈路帶寬消耗量。

2.2 基于SMT求解器的虛擬網映射問題求解

2.2.1SMT求解器

用以求解SMT問題的自動化工具稱為SMT求解器。SMT求解器的算法實現分為兩類，第一類是積極類算法，它將SMT公式轉化為SAT公式，然后用SAT求解器求解；第二類是惰性算法，它將SMT公式層次化為布爾公式與理論公式，然后采用SAT求解器與理論求解器互動求解[13]。

積極類算法將SMT公式轉化為SAT公式時，SAT公式長度隨問題規模呈指數型增長，故不適用于大規模問題求解。而惰性算法通過SAT求解器與理論求解器互相配合，提高了問題求解效率，成為大多數SMT求解器的選擇。

目前，主流SMT求解器支持的背景理論有整數集上的線性算數理論(quantifier free_linear integer arithmetic，QF_LIA)、實數集上的線性算數理論(quantifier free_linear real arithmetic，QF_LRA)、數組理論、未解釋函數理論等[13]。

2.2.2 虛擬網映射問題求解

(|Ns|-1)]進行二分搜索，該區間的下界是虛擬網絡所有鏈路的帶寬之和，表示每條虛擬鏈路所映射的物理路徑的長度至少為1；上界是虛擬網絡所有鏈路的帶寬之和與物理節點數減1之乘積，表示每條虛擬鏈路所映射的物理路徑的長度至多為物理節點數減1。OPT-MathSA[15]、Z3[16]和SYMBA[17]等SMT求解器均能滿足問題求解需要。

3 平均性能實驗評估

基于SMT求解器的虛擬網映射問題精確求解方法屬于一階段映射精確算法。目前提出的求解虛擬網映射問題的精確算法，其本質是求解混合整數線性規劃模型的不同方法，主要包括列生成算法(Column Generation Algorithm，CGA)[9]、最優分解法(optimal decomposition approach，ODA)[10]和采用優化軟件的分枝定界法等[11-12]。

下面采用實驗的方法評估基于SMT求解器的虛擬網映射問題精確求解方法的平均性能，具體把所提出的基于SMT求解器的方法同列生成算法[9]、最優分解算法[10]和基于優化軟件方法[12]進行比較，虛擬網映射問題的線性整數規劃數學模型采用VNM_IP。

3.1 實驗環境及性能評估指標

基于Mininet和FlowVisor[18]構建仿真環境，SMT求解器采用Z3 4.4.4，優化軟件CPLEX采用CPLEX11.0，優化軟件LINGO采用LINGO 11.0。本實驗在配置Intel(R) Core(TM) i5- 480M@ 2.67 GHz CPU，4 GB內存的電腦上進行。對基于Z3求解虛擬網映射問題的性能分析，主要使用虛擬網請求接受率、單位時間物理網絡提供商的平均收益和求得虛擬網映射問題最優解所用平均時間等三個評估指標。

3.2 實驗數據的設定

物理網絡和虛擬網絡構建采用當前研究常用的方法[2]，即采用GT-ITM[2]工具構建物理節點CPU容量和物理鏈路帶寬均在[480,580]內均勻分布的包含30個物理節點和40條物理鏈路的物理網絡。虛擬網絡的到達是平均每5分鐘有1.3個請求的泊松過程，每個虛擬網絡的生存時間符合均值為5 000分鐘的指數分布；虛擬網絡的虛擬節點數在[2,5]間均勻分布，虛擬網絡的連通度是50%，虛擬節點CPU容量和虛擬鏈路帶寬均在[1,6]內均勻分布。另外，求解每個虛擬網映射問題的時間限定在4分鐘之內。

3.3 實驗結果及分析

實驗發現采用優化軟件CPLEX和LINGO求解性能相差很小，故下面針對采用優化軟件CPLEX的結果進行分析。

(1) 基于SMT求解器的求解法提高了請求接受率和長期收益。圖1和圖2表明前750個虛擬網絡請求到達后所有算法都能夠完成構建，但隨著時間的推移和請求數的不斷增加，所有算法的請求接受率和平均收益就相對穩定。基于SMT求解器的求解方法的請求接受率穩定在0.809左右，比列生成算法CGA、最優分解算法ODA和基于優化軟件CPLEX的方法分別提高19.2%、15.5%和9.6%；物理網絡提供商單位時間(設為5分鐘)平均收益穩定在17 283左右，比列生成算法CGA、最優分解算法ODA和基于優化軟件CPLEX的方法分別提高20.1%、16.6%和10.9%。因虛擬網請求接受率等同于求得虛擬網映射問題最優解比例，故基于SMT求解器的求解方法求得虛擬網映射問題最優解比例穩定在0.809左右，比其他三種算法至少提高9.6%。

圖1 虛擬網構建請求接受率

圖2 物理網提供商平均收益

(2) 基于SMT求解器的求解法的最優解平均求解時間更短。從圖3可觀察到基于SMT求解器的求解方法，求得虛擬網映射問題最優解所用平均時間在3.43分鐘左右，比列生成算法CGA、最優分解算法ODA和基于優化軟件CPLEX的方法分別減少2.9%、8.1%和9.4%。從圖1和圖2可知，相比于列生成算法CGA、最優分解算法ODA和基于優化軟件CPLEX的方法，基于SMT求解器的求解方法的物理網提供商單位時間平均收益提高幅度高于虛擬網請求接受率提高幅度至少0.9%，說明在限定時間內基于SMT求解器的求解方法能夠求解出更加復雜的虛擬網映射請求，可以得出基于SMT求解器的實際求解方法的求解效率比圖3所示結果更優。

圖3 最優解平均求解時間

4 結 語

針對物理網不支持路徑分割且物理節點不支持重復映射的虛擬網映射問題，基于可滿足性模理論，構建解決虛擬網映射問題的SMT公式，并采用SMT求解器求解最優解。實驗表明，與目前基于求解混合整數線性規劃模型的精確算法相比，基于可滿足性模理論的虛擬網映射問題求解精確方法，具有更高的有效性和實用性。后期，將對如何進一步優化虛擬網映射問題的SMT公式繼續開展研究，以進一步提高求解效率。