智慧來
河南理工大學計算機科學與技術(shù)學院,河南焦作 454000
同一變量排序下的多OBDD合并算法
智慧來
河南理工大學計算機科學與技術(shù)學院,河南焦作 454000
有序決策圖(OBDD)是一種用于表示布爾表達式的數(shù)據(jù)結(jié)構(gòu),并在許多領(lǐng)域得到了廣泛應用。在分布式或者動態(tài)環(huán)境下,利用已知布爾表達式的OBDD構(gòu)造目標布爾表達式的OBDD是一個決定實際問題解決效率的關(guān)鍵問題?;赟hannon分解原理提出了一個同一變量排序下的OBDD合并算法。該算法首先建立目標布爾表達式的表存儲模型,然后按照變量排序的逆序,依次處理各個變量,并且合并取值相同的行,直到所有變量處理完畢。
有序決策圖(OBDD);同一變量排序;多有序決策圖(OBDD)合并;Apply算法
有序二叉決策圖(Ordered Binary Decision Diagram,OBDD)是一種用于表示布爾函數(shù)的數(shù)據(jù)結(jié)構(gòu)[1-2],是迄今為止最為有效的符號技術(shù)之一。OBDD已經(jīng)應用在粗糙集屬性約簡表示[3]、局部模式挖掘[4]、并行電力系統(tǒng)恢復[5]、網(wǎng)絡可靠性分析[6-7]、約束滿足問題求解[8-10]等眾多領(lǐng)域。
在分布式或者是動態(tài)環(huán)境下,利用已知布爾函數(shù)的OBDD構(gòu)造目標布爾函數(shù)的OBDD是一個關(guān)鍵技術(shù)問題。譬如,已知f1、f2和f3的OBDD,構(gòu)造一個目標表達式f=f1∨(f2∧┐f3),f的OBDD如何構(gòu)造?
Colorado大學開發(fā)的CUDD軟件包[11],里面包含有Apply操作,即
此操作輸入表達式u1和u2的OBDD,返回表達式u1op u2的OBDD,其中op是布爾運算符。
一個顯而易見的方法是首先構(gòu)造┐f3的OBDD,然后使用Apply算法求出f2∧┐f3的OBDD,最后再一次使用Apply算法求出的f1∨(f2∧┐f3)的OBDD。顯然,上述過程兩次使用了Apply算法,且每次使用Apply算法都是基于Shannon分解原理的。
到目前為止,現(xiàn)有的研究均是針對兩個表達式的OBDD合成,都沒有涉及多個表達式的OBDD合成。例如,古天龍等[12]指出,給定集合S和T,并已知它們的布爾函數(shù),則集合S和T的并、交和差運算等布爾運算都可以由相應的OBDD操作來高效地加以實現(xiàn)。愛丁堡大學的Paul Jackson[13]也對OBDD操作做了總結(jié)性的研究,指出可以利用Shannon分解原理以及Apply算法對兩個表達式的OBDD進行合成。
鑒于上述分析,本文將在Shannon分解原理的基礎(chǔ)上,提出一個同一變量排序下的多OBDD合并算法,用以構(gòu)造復合布爾表達式的OBDD。
OBDD是布爾表達式的一種有效表示方法,它具有規(guī)范性,即在給定的變量排序下,任一給定的布爾表達式所對應的OBDD是最簡且唯一的。
當繪制OBDD時,0分支用虛線表示,1分支用實線表示,輸出值0和1用葉子結(jié)點表示。OBDD結(jié)構(gòu)體現(xiàn)了Shannon分解原理,即每一個結(jié)點都是一個ite(if-then-else)結(jié)構(gòu)。如果用x→f1,f2表示一個ite(x,f1,f2)結(jié)構(gòu),則有以下的定義:
顯然,一個ite(x,f1,f2)結(jié)構(gòu)的意義是:若x成立,則選擇f1分支;否則,選擇f2分支。
在下文中,f[0/x]表示將表達式f中的變量x用0替換,f[1/x]表示將表達式f中的變量x用1替換,顯然有:f=x→f[0/x],f[1/x],并簡寫為f=x→f0,f1。
例1有三個布爾表達式f1,f2,f3如下:
上述三個布爾表達式f1,f2,f3的OBDD如圖1(a)(b)(c)。
另外,還可以采用表格的方式來存儲一個OBDD,方式如下:每一行存儲一個結(jié)點的信息;第一列存儲是結(jié)點的標識;第二列,即表頭為var的列,存儲的是結(jié)點表示的變量;第三列,即表頭為0的列,存儲的是結(jié)點的0分支;第四列,即表頭為1的列,存儲的是結(jié)點的1分支。
對于例1中的三個布爾表達式,對應OBDD的表存儲方式見表1(a)(b)(c)。
表1 (a)f1的存儲表
表1 (b)f2的存儲表
表1 (c)f3的存儲表
給定義組布爾表達式f1,f2,…,fm,則可以使用邏輯連接符┐,∨,∧,→,?構(gòu)造出新的布爾表達式t,即t= F(f1,f2,…,fm),F(xiàn)表示f1,f2,…,fm的函數(shù)。
同一變量排序下的多OBDD合并,即從f1,f2,…,fm的OBDD出發(fā),構(gòu)造布爾表達式t的OBDD。
算法1同一變量排序下的多OBDD合并算法
輸入f1,f2,…,fm的OBDD,布爾表達式t=F(f1,f2,…,fm)
輸出布爾表達式t的OBDD
步驟1建立f1,f2,…,fm的OBDD對應的存儲表。
圖1 (a)布爾表達式f1的OBDD1
圖1 (b)布爾表達式f2的OBDD2
圖1 (c)布爾表達式f3的OBDD3
步驟2初始化t的OBDD對應的存儲表如表2所示,每一行存儲一個結(jié)點,并在存儲表的右側(cè)增加m列,分別存儲該結(jié)點在OBDD1,OBDD2,…,OBDDm中的位置。
表2 初始存儲表
步驟3處理變量xn,使用式子F((t00..00)1,…,(t00..00)m)、F((t00..01)1,…,(t00..01)m)、…、F((t00..01)1,…,(t00..01)m)計算t00..00、t00..01、…、t11..11的值(共2n-1個)。
同時,對于t00..00、t00..01、…、t11..11中的每一個行,若取值為(0,0)或(1,1),則將這一行用0或1代替;若t00..00、t00..01、…、t11..11中存在相同的行,則將這些行用同一標識進行標記。
步驟4設置循環(huán)變量i并賦初值n-1,當i>0時循環(huán)執(zhí)行以下操作:
步驟4-1將變量2i個變量xi+1的值填寫到2i-1個變量xi的0分支和1分支當中。
步驟4-2若取值為(0,0)或(1,1),則將這一行用0或1代替。
步驟4-3在標記個變量xi的這2i-1行中,若存在相同的行,則將這些行用同一標識進行標記。
步驟4-4將循環(huán)變量i減1,若i>0,則執(zhí)行步驟4-1,否則循環(huán)結(jié)束。
步驟5刪除冗余行并對結(jié)點進行編號,得到最終的存儲表。
步驟6依據(jù)存儲表建立表達式的OBDD,算法結(jié)束。
布爾表達式t=F(f1,f2,…,fm)中變量的數(shù)目決定了存儲表的規(guī)模,存儲變量x1,x2,…,xn所占用的空間是一個公比為2的等比數(shù)列,因此算法1的空間復雜度為O(2n)。若以處理一行的時間作為衡量算法復雜性的單位時間,那么算法1的時間復雜度為T(2n)。與Apply算法相比,Apply算法一次只能處理一對表達式,而本文的算法能夠一次處理任意多個表達式,提高了構(gòu)造OBDD的效率。
例1(續(xù))f=f1∨(f2∧┐f3),構(gòu)造f的OBDD。
步驟1建立f1,f2,f3的OBDD對應的存儲表,見表1(a)(b)(c)。
步驟2初始化t的OBDD對應的存儲表,如表3所示。
表3 表達式t的初始化存儲表
步驟3處理變量x3,計算t00、t01、t10、t11,即
并將t00行的標識修改為0,將t10行的標識修改為1;又因為t01和t11相同,所以將t11的標識修改為t01。
步驟4依次處理變量x2,x1:
對變量x2的處理:對于結(jié)點t0,0分支為t00,由于t00的標識已經(jīng)修改為0,因此t0的0分支修改為0;對于結(jié)點t0,0分支為t10,由于t10的標識已經(jīng)修改為1,因此t0的0分支修改為1。
對變量x1沒有修改,最后得到存儲表見表4。
表4 表達式t的存儲表
步驟5刪除冗余行并對結(jié)點進行編號,得到最終的存儲表見表5。
步驟6依據(jù)存儲表建立表達式的OBDD,結(jié)果見圖2。
表5 重新編號后表達式t的存儲表
圖2 布爾表達式f1∨(f2∧┐f3)的OBDD
在OBDD的應用中,利用已知布爾函數(shù)的OBDD構(gòu)造目標布爾函數(shù)的OBDD是一個關(guān)鍵問題。本文利用OBDD的表存儲模型,基于Shannon分解原理提出了一個同一變量排序下的OBDD合并算法。與Apply算法相比,Apply算法一次只能處理一對表達式,而本文的算法能夠一次處理任意多個表達式,提高了構(gòu)造OBDD的效率。
[1]Akers S B.Binary decision diagrams[J].IEEE Transactions on Computer,1978,27(6):509-516.
[2]Bryant R E.Graph based algorithms for Boolean function manipulation[J].IEEE Transactions on Computer,1986,35(8):677-691.
[3]Wei Qianjin,Gu Tianlong.Symbolic representation for rough set attribute reduction using ordered binary decision diagrams[J].Journal of Software,2011,6(6):977-984.
[4]Yang Liu,M anadhata P K,Horne W G,et al.Fast submatch extraction using OBDDs[R].[S.l.]:HP Laboratories,2012.
[5]Wang Chong,Vittal V,Sun K.OBDD-based sectionalizing strategies for parallel power system restoration[J].IEEE Transactions on Power System s,2011,26(3):1426-1433.
[6]陳瑤,李峭,趙長嘯,等.基于OBDD的航空電子網(wǎng)絡可靠性分析[J].系統(tǒng)工程與電子技術(shù),2013,35(1):230-236.
[7]趙勃,肖宇峰,劉巖.基于OBDD的通信網(wǎng)鏈路重要性評估[J].系統(tǒng)工程與電子技術(shù),2011,33(10):2348-2352.
[8]徐周波,古天龍,常亮,等.約束滿足問題求解的符號OBDD桶消元算法[J].計算機科學,2011,38(7):200-203.
[9]徐周波,古天龍.裝配序列規(guī)劃問題的CSP模型及其符號OBDD求解技術(shù)[J].計算機輔助設計與圖形學學報,2010,22(5):803-810.
[10]古天龍,楊志飛.基于有序二叉決策圖的裝配序列符號表示方法[J].計算機輔助設計與圖形學學報,2007,19(10):1315-1320.
[11]Somenzi F.CUDD:CU decision diagram package release 2.4.1[EB/OL].[2013-09-11].http://vlsi.Colorado.edu/fabio/ CUDD/cudd Intro.htm l.
[12]古天龍,呂思菁,常亮,等.基于OBDD的描述邏輯εL循環(huán)術(shù)語集推理[J].軟件學報,2014,25(1):64-77.
[13]Jackson P.BDD operations[EB/OL].[2013-12-21].www.inf. ed.ac.uk/teaching/courses/ar/slides/bdd-ops.pdf.
ZHI Huilai
School of Computer Science and Technology, Henan Polytechnic University, Jiaozuo, Henan 454000, China
Ordered Binary Decision Diagrams(OBDD)is a Boolean function representation data structure, and has been applied in many fields. In dynamic or distribute environment, how to efficiently build OBDD of the target Boolean expression form the known Boolean expression’s OBDD is a frequent encountered problem. Under identical variable ordering,this paper puts forward a OBDD merging algorithm based on Shannon decomposition principle. In the algorithm, it firstly establishes a storage table for the target Boolean expression, and then under the reverse variable ordering it handles each variable in turn, and combines the rows with same values, until all the variables are handled.
words:Ordered Binary Decision Diagrams(OBDD); identical variable ordering; multiple Ordered Binary Decision Diagrams(OBDD)merging; Apply algorithm
ZHI Huilai. Multiple OBDD merging algorithm under same variable ordering. Computer Engineering and Applications,2014, 50(17):20-23.
A
TP18
10.3778/j.issn.1002-8331.1312-0067
國家自然科學基金(No.60975033);河南理工大學博士基金(No.B2011-102)。
智慧來(1981—),男,博士,講師,研究領(lǐng)域包括形式概念分析、知識表示與推理等。E-mail:zhihuilai@126.com
2013-12-05
2014-03-10
1002-8331(2014)17-0020-04
CNKI網(wǎng)絡優(yōu)先出版:2014-03-19,http://www.cnki.net/kcms/doi/10.3778/j.issn.1002-8331.1312-0067.htm l