• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    基于模型診斷中結(jié)合問(wèn)題特征的新方法

    2017-04-07 07:00:52歐陽(yáng)丹彤周建華劉伯文張立明
    關(guān)鍵詞:枚舉子句診斷系統(tǒng)

    歐陽(yáng)丹彤 周建華 劉伯文 張立明

    1(吉林大學(xué)軟件學(xué)院 長(zhǎng)春 130012)2(吉林大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 長(zhǎng)春 130012)3 (符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué)) 長(zhǎng)春 130012)(15943054244@163.com)

    基于模型診斷中結(jié)合問(wèn)題特征的新方法

    歐陽(yáng)丹彤1,2,3周建華1,3劉伯文2,3張立明1,2,3

    1(吉林大學(xué)軟件學(xué)院 長(zhǎng)春 130012)2(吉林大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 長(zhǎng)春 130012)3(符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué)) 長(zhǎng)春 130012)(15943054244@163.com)

    基于模型診斷一直是人工智能領(lǐng)域中熱門的研究問(wèn)題.近些年來(lái),隨著SAT求解器效率的逐漸提高,基于模型的診斷也被轉(zhuǎn)換成SAT問(wèn)題進(jìn)行求解.在對(duì)基于模型診斷求解方法CSSE-tree深入研究基礎(chǔ)上,結(jié)合診斷問(wèn)題和SAT求解過(guò)程的特征,給出先對(duì)包含組件個(gè)數(shù)較多的候選診斷進(jìn)行求解的方法,進(jìn)而減小SAT求解問(wèn)題的規(guī)模;在對(duì)極小診斷解和非極小診斷解剪枝方法的基礎(chǔ)上,首次提出非診斷解定理及非診斷解空間的剪枝方法,有效地實(shí)現(xiàn)了對(duì)診斷的無(wú)解空間進(jìn)行剪枝.根據(jù)組件個(gè)數(shù)較多的候選診斷先求解及有解無(wú)解剪枝方法特征,構(gòu)建基于反向搜索的LLBRS-tree方法.實(shí)驗(yàn)結(jié)果表明:與CSSE-tree算法相比,LLBRS-tree算法減少了SAT求解次數(shù)、減小了求解問(wèn)題規(guī)模,效率較好,尤其是求解多診斷時(shí)效率提高更為顯著.

    基于模型的診斷;無(wú)解空間剪枝;合取范式;SAT求解器;枚舉樹

    自1980年至今,基于模型診斷(model-based diagnosis, MBD)在人工智能領(lǐng)域一直是一個(gè)熱門的研究問(wèn)題,對(duì)人工智能領(lǐng)域的推進(jìn)起到了十分重要的作用.最早的模型診斷方法由Reiter[1]于1987年提出,求解最終診斷結(jié)果的過(guò)程分為2個(gè)步驟:1)產(chǎn)生所有極小沖突集的沖突識(shí)別;2)產(chǎn)生所有極小碰集的候選產(chǎn)生.這2個(gè)步驟在得到最后的診斷結(jié)果中起著重要作用.國(guó)內(nèi)外學(xué)者對(duì)碰集求解方法做了許多研究和改進(jìn).碰集的求解方法主要分為基于枚舉的完備性算法[2-5]和基于局部搜索的非完備性算法[6-7].完備性算法雖然可以準(zhǔn)確給出碰集問(wèn)題的所有解,但隨著碰集問(wèn)題規(guī)模的增大,求解時(shí)間也會(huì)隨之以指數(shù)級(jí)增加.基于局部搜索的非完備性算法雖然不確定能給出特定的解,但對(duì)于大規(guī)模問(wèn)題有較好效率.

    國(guó)內(nèi)學(xué)者在模型診斷方法研究上也做了大量相關(guān)的工作.張健等人[8-9]給出了將診斷問(wèn)題轉(zhuǎn)換為布爾公式和數(shù)學(xué)公式的混合形式描述,然后用帶有標(biāo)志子句技術(shù)的求解器進(jìn)行診斷;姜云飛等人[10]在候選診斷的分解與組合問(wèn)題上給出了基于分步求解的診斷分解的方法;趙相福等人[11-13]提出利用SAT求解器來(lái)判斷一個(gè)組件集合是否是系統(tǒng)的診斷解,然后結(jié)合CSSE-tree求出所有的極小診斷求解方法;陳榮等人[14]先利用SAT求解器得到診斷系統(tǒng)對(duì)應(yīng)的沖突部件集,然后對(duì)沖突部件集調(diào)用碰集算法得到系統(tǒng)的候選診斷;歐陽(yáng)丹彤等人[15]提出通過(guò)在診斷系統(tǒng)中傳播元件的輸出標(biāo)識(shí),來(lái)判斷當(dāng)前候選元件集合是否為系統(tǒng)的候選診斷的方法;欒尚敏等人[16]提出結(jié)合系統(tǒng)結(jié)構(gòu)信息來(lái)求解極小沖突集和直接求解候選診斷的方法.以上給出的診斷方法或是提高了診斷求解效率,或是減小了求解時(shí)的內(nèi)存空間消耗.

    命題可滿足問(wèn)題(propositional satisfiability problem,SAT)是人工智能領(lǐng)域中很活躍的一個(gè)分支,它是NP完全問(wèn)題[17-19].人工智能中很多NP完全問(wèn)題都可以轉(zhuǎn)換為SAT問(wèn)題,然后進(jìn)行求解,而且隨著SAT求解器效率的提高,越來(lái)越多的NP問(wèn)題都先轉(zhuǎn)化為SAT問(wèn)題,然后進(jìn)行求解[20-22].如智能規(guī)劃問(wèn)題以及模型檢測(cè)問(wèn)題都可以轉(zhuǎn)化為SAT問(wèn)題進(jìn)行求解[23].相應(yīng)地,MBD問(wèn)題也可以轉(zhuǎn)換成SAT問(wèn)題來(lái)求解.基于SAT求解器的發(fā)展,以及根據(jù)將基于模型的診斷轉(zhuǎn)換成SAT問(wèn)題求解的思想,國(guó)內(nèi)學(xué)者趙相福等人給出的利用SAT求解器結(jié)合CSSE-tree求出所有的極小診斷解.在判斷一個(gè)組件集合是否是系統(tǒng)的診斷時(shí),該文將要判斷的組件集合的補(bǔ)集中所有組件的正常行為謂詞描述、系統(tǒng)描述和觀測(cè)描述3部分文件構(gòu)造成一個(gè)CNF文件,然后調(diào)用SAT求解器去判斷可滿足性,如果可滿足,則是診斷解.基于這樣的基礎(chǔ),該文結(jié)合CSSE-tree樹模型,根據(jù)組件集合的個(gè)數(shù),枚舉出組件集合的所有冪集合,然后進(jìn)行一一的判斷.而且為了更加高效地求解,本文提出了2個(gè)優(yōu)化策略:1)從根結(jié)點(diǎn)開始,利用廣度優(yōu)先遍歷,對(duì)長(zhǎng)度小的集合先判斷,直接先得到最終的極小診斷解;2)根據(jù)CSSE-tree的生成方式,利用極小診斷解的真超集一定不是極小診斷解的剪枝規(guī)則,將極小診斷解的子結(jié)點(diǎn)全部剪掉.但是,給合實(shí)際的診斷實(shí)例特征,我們可以知道在CSSE-tree中只有較少的結(jié)點(diǎn)是極小診斷解,該方法中的修剪規(guī)則只針對(duì)有解的那些結(jié)點(diǎn),所以剪掉的結(jié)點(diǎn)數(shù)量較少.

    針對(duì)CSSE-tree中只對(duì)是解的結(jié)點(diǎn)進(jìn)行剪枝這樣的缺點(diǎn),我們?cè)诒疚闹刑岢隽嘶诜聪蛩阉鞯挠薪鉄o(wú)解剪枝方法LLBRS-tree.在該方法中我們不僅剪掉是解的結(jié)點(diǎn),而且第1次提出了無(wú)解剪枝的思想,對(duì)不是解的那些結(jié)點(diǎn)也進(jìn)行剪枝.并且在利用SAT求解器來(lái)判斷一個(gè)組件集合是否是診斷解時(shí),我們首先對(duì)長(zhǎng)度比較長(zhǎng)的組件集合進(jìn)行處理,使得生成的CNF形式的文件中要判斷的子句的數(shù)量較少,因此調(diào)用SAT求解器來(lái)判斷時(shí)所耗費(fèi)的時(shí)間也將更少.

    1 預(yù)備知識(shí)

    在本節(jié),我們首先介紹基于模型的診斷中的相關(guān)概念,而后介紹SAT問(wèn)題,最后介紹將基于模型的診斷轉(zhuǎn)換成SAT問(wèn)題.

    1.1 基于模型的診斷的相關(guān)概念

    定義1. 診斷系統(tǒng)[1].一個(gè)系統(tǒng)定義為一個(gè)三元組(SD,COMPS,OBS),其中:SD為系統(tǒng)描述,是一階謂詞公式的集合;COMPS為系統(tǒng)的組成部件集合,是一個(gè)有限常量集合;而OBS為觀測(cè)集合,是一階謂詞公式的有限集合.

    在下面我們使用一元謂詞AB(·)表示“abnormal”,AB(c)為真當(dāng)且僅當(dāng)c反常,其中c∈COMPS.

    定義2. 基于一致性診斷[1].設(shè)組件集合Δ?COMPS,稱Δ為關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷,如果SD∪OBS∪{AB(c)|c∈COMPS-Δ}是可滿足的.

    定義3. 極小診斷集[1].稱一個(gè)關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷Δ是極小的,當(dāng)且僅當(dāng)不存在Δ的任何真子集也是關(guān)于(SD,COMPS,OBS)的一個(gè)基于一致性診斷.

    通過(guò)上面的定義可以知道,我們要判斷一個(gè)組件集合是否是系統(tǒng)的一個(gè)基于一致性的診斷集,只需要判定這個(gè)組件集合中的所有組件為反常的情況下,剩余組件的正常行為描述與診斷系統(tǒng)相關(guān)的系統(tǒng)描述以及系統(tǒng)觀測(cè)描述的邏輯是否是一致的.

    而且,根據(jù)基于一致性診斷的極小診斷集的定義可以得到下面的結(jié)論:如果組件集合A是系統(tǒng)的一個(gè)基于一致性診斷的極小診斷集,且組件集合B?COMPS,組件集合C?COMPS,則有2種情況:

    1) 如果組件集合A?B,那么組件集合B不是基于一致性診斷的極小診斷集;

    2) 如果組件集合C?B且B不是診斷解,那么組件集合C一定不是診斷解.

    上面的情況表明一個(gè)極小診斷集的真超集一定不是極小診斷集;并且進(jìn)一步說(shuō)明如果一個(gè)組件集合不是診斷解,那么它的真子集一定不是診斷解.這2種情況是我們判斷診斷解以及極小診斷集的基礎(chǔ).

    1.2 SAT問(wèn)題

    首先,我們將要用到的符號(hào)定義如下:

    變量xi(i=1,2,…,m)表示布爾變量;X={x1,x2,…,xm}表示變量的集合;在子句中我們用符號(hào)xi表示與變量xi相對(duì)應(yīng)的正文字,符號(hào)xi表示與變量xi相對(duì)應(yīng)的負(fù)文字;符號(hào)Ci(i=1,2,…,n)表示子句,子句由文字的析取構(gòu)成,我們可以將子句看作是文字的集合.符號(hào)Φ,Φi(i=1,2,3,…)代表CNF公式,CNF公式是由子句的合取構(gòu)成,可以將它看成是子句的集合.在本文中,命題公式指的就是CNF公式.

    SAT問(wèn)題又叫做命題可滿足問(wèn)題,即判斷給定的一個(gè)命題公式是不是可滿足的,其形式化的定義如下:

    定義4. 命題可滿足問(wèn)題[19].針對(duì)給定的一個(gè)命題公式Φ,X={x1,x2,…,xm}是該公式的變量集合,SAT問(wèn)題是指是否存在一組X的賦值使得Φ的取值為真.如果存在這樣的一組賦值,那么我們則稱命題公式Φ是可滿足的,否則Φ是不可滿足的.

    根據(jù)SAT問(wèn)題的定義,我們只需要找到一組賦值使得給定的命題公式的取值為真,就可以判定該命題公式是可滿足的.

    迄今為止,許多學(xué)者都投入到SAT問(wèn)題的研究中來(lái),每年舉行一次的SAT競(jìng)賽也使得很多成熟高效的SAT求解器產(chǎn)生.對(duì)于常規(guī)的SAT求解器,都是以CNF形式的文件作為SAT求解器的輸入.針對(duì)給定的命題公式或者命題公式集合,都可以將其轉(zhuǎn)化成一個(gè)CNF形式的文件描述.例如:給定的一個(gè)命題公式集合R:{x1→x2,x2→x3,x3→x4,x4,x1},我們可以將其表示為下面的一個(gè)CNF文件.使用數(shù)字1,2,3,4分別表示公式R中的變量x1,x2,x3,x4:

    -3 4 0

    -4 0

    1 0

    經(jīng)過(guò)上面的轉(zhuǎn)化,判定命題公式集合R是否為真時(shí),只需要將公式R轉(zhuǎn)換成CNF文件描述,接下來(lái)調(diào)用SAT求解器對(duì)轉(zhuǎn)換后的CNF文件進(jìn)行求解就可以得到結(jié)果.如果CNF文件是可滿足的,那么命題公式R為真,否則公式R為假.

    根據(jù)上面的這種思想,我們要判斷一個(gè)組件集合S是否是一個(gè)系統(tǒng)的一個(gè)基于一致性的診斷,只需要假設(shè)要判斷的組件集合S為診斷解,將COMPS-S集合中每一個(gè)組件相關(guān)的正常子句描述,系統(tǒng)描述以及系統(tǒng)的觀測(cè)描述一起構(gòu)建成一個(gè)CNF形式的文件,接下來(lái)調(diào)用SAT求解器進(jìn)行可滿足性判定即可.如果SAT求解器返回真值,那么S是系統(tǒng)的一個(gè)基于一致性診斷解.否則,S不是.

    1.3 基于模型的診斷轉(zhuǎn)換成SAT問(wèn)題

    在本節(jié),將介紹如何將診斷系統(tǒng)的模型以及系統(tǒng)的觀測(cè)轉(zhuǎn)換成CNF形式的文件.

    給定一個(gè)診斷系統(tǒng),本文中對(duì)其進(jìn)行建模的方式與Reiter[1]建模的方法不同,我們將使用命題邏輯對(duì)該系統(tǒng)相關(guān)的行為進(jìn)行建模.我們將使用變量來(lái)表示系統(tǒng)中的相關(guān)組件的輸入以及輸出,并且我們將對(duì)每個(gè)組件進(jìn)行編號(hào).跟診斷系統(tǒng)的定義一樣,我們也使用AB(c)和AB(c)來(lái)表示組件屬于反常模式或者正常模式.

    以圖1所表示的ISCAS-85_c17為例,介紹我們是如何對(duì)診斷系統(tǒng)進(jìn)行建模,得到相對(duì)應(yīng)的CNF文件描述.根據(jù)ISCAS-85_c17的Verilog電路描述,我們得到圖1所示的邏輯電路.在該邏輯電路中有6個(gè)組件,都是與非門,分別用N1,N2,N3,N4,N5,N6來(lái)標(biāo)識(shí)出6個(gè)邏輯與非門.而“7”,“8”,“9”,“10”,“11”分別表示系統(tǒng)相應(yīng)的輸入變量,“12”,“13”分別表示系統(tǒng)的輸出變量,“14”,“15”,“16”,“17”分別表示組件內(nèi)部的連接結(jié)點(diǎn).例如變量“14”既表示組件N2的輸出,又是組件N3的輸入.

    Fig. 1 Logic circuit of ISCAS-85_c17圖1 ISCAS-85_c17邏輯電路

    為了將系統(tǒng)最后轉(zhuǎn)換成CNF文件的形式進(jìn)行描述,我們需將該邏輯電路ISCAS-85_c17采用CNF文件的編碼,并進(jìn)行相應(yīng)地轉(zhuǎn)換.最后,我們得到邏輯電路ISCAS-85_c17的部分CNF文件描述為C17.cnf,如圖2所示.

    Fig. 2 C17.cnf圖2 C17.cnf

    圖2所給的僅僅是部分系統(tǒng)描述,相應(yīng)地,我們還需要對(duì)系統(tǒng)的觀測(cè)給出CNF形式的描述.例如,當(dāng)邏輯電路ISCAS-85_c17當(dāng)前得到的觀測(cè)值為:輸入觀測(cè)點(diǎn)“7”,“8”,“9”,“10”,“11”的觀測(cè)分別為高電平,低電平,低電平,高電平,高電平;輸出觀測(cè)點(diǎn)“12”,“13”的觀測(cè)值為高電平,低電平.則我們得到系統(tǒng)觀測(cè)的CNF子句描述如下:

    7 0

    -8 0

    -9 0

    10 0

    11 0

    12 0

    -13 0

    通過(guò)上面這樣的轉(zhuǎn)換方式,我們就可以將一個(gè)診斷系統(tǒng)轉(zhuǎn)換成相應(yīng)的CNF文件描述,也就是轉(zhuǎn)換成SAT問(wèn)題,然后針對(duì)該CNF文件進(jìn)行相應(yīng)地處理,調(diào)用SAT求解器對(duì)其進(jìn)行求解,最后得到診斷系統(tǒng)的診斷解,具體的算法我們?cè)诘?節(jié)進(jìn)行介紹.

    2 用ISDAG算法結(jié)合枚舉樹求解所有診斷

    在第1節(jié)我們將一個(gè)診斷系統(tǒng)轉(zhuǎn)換成SAT問(wèn)題,本節(jié)將首先介紹判斷一個(gè)組件集合是否是診斷解的算法ISDAG,然后講解利用ISDAG算法,結(jié)合枚舉樹來(lái)求解一個(gè)給定診斷系統(tǒng)的所有基于一致性診斷的極小診斷解.

    2.1 ISDAG算法

    我們給出如下的一些定義,方便對(duì)算法進(jìn)行描述.

    定義5. 反常單元子句表示.對(duì)于給定的一個(gè)組件,該組件的反常單元子句表示是指用正文字單元子句描述該組件.

    定義6. 正常單元子句表示.對(duì)于給定的一個(gè)組件,該組件的正常單元子句表示是指用負(fù)文字單元子句描述該組件.

    例如:組件N1,我們用數(shù)字“1”代表這個(gè)組件,那么組件N1的反常單元子句表示如下:

    組件N1的正常單元子句表示如下:

    當(dāng)給定一個(gè)診斷系統(tǒng)后,假設(shè)系統(tǒng)所對(duì)應(yīng)的描述以及觀測(cè)都已經(jīng)通過(guò)離線方式創(chuàng)建完成,正如在1.3節(jié)所述.假設(shè)系統(tǒng)描述的文件為DigSysDis.cnf以及DigSysObs.cnf,下面的ISDAG算法將介紹如何使用SAT求解器來(lái)判斷一個(gè)組件集合是否是給定診斷系統(tǒng)的基于一致性診斷的診斷解.

    算法1. ISDAG(Sub[])算法.

    輸入:將要判斷系統(tǒng)的一個(gè)組件子集Sub;

    輸出:bool類型值,如果組件子集Sub是系統(tǒng)的基于一致性診斷,則返回1,否則返回0.

    Step1. 將系統(tǒng)的觀測(cè)文件DigSysObs.cnf中的子句追加到系統(tǒng)描述文件DigSysDis.cnf中.

    Step2. 對(duì)于在組件集合Sub中的每一個(gè)組件,將其對(duì)應(yīng)的反常單元子句表示(相當(dāng)于一個(gè)選擇器,表明假設(shè)該組件集合都發(fā)生故障的情況)追加到系統(tǒng)描述文件DigSysDis.cnf中.

    Step3. 對(duì)于在組件集合(COMPS-Sub)中的每一個(gè)組件,將其對(duì)應(yīng)的正常單元子句表示(表明這些組件都正常工作,沒(méi)有發(fā)生故障)追加到系統(tǒng)描述文件DigSysDis.cnf中.

    Step4. 調(diào)用SAT求解器對(duì)系統(tǒng)文件DigSysDis.cnf進(jìn)行可滿足性判斷,如果得到的結(jié)果是可滿足的,那么表明組件集合Sub是診斷解,返回1.如果得到的結(jié)果是不可滿足的,那么表明組件集合Sub不是診斷解,返回0.

    針對(duì)ISDAG算法中的Step2,Step3我們舉例說(shuō)明,假設(shè)COMPS={N1,N2,N3,N4,N5,N6},而Sub={N1,N2,N3}時(shí),那么在執(zhí)行Step2以及Step3后,我們加入到DigSysDis.cnf文件中的子句如下:

    1 0

    2 0

    3 0

    -4 0

    -5 0

    -6 0

    我們要判斷一個(gè)組件子集Sub是否是系統(tǒng)的診斷,首先需要將系統(tǒng)的觀測(cè)都追加到系統(tǒng)描述文件中,然后在考慮組件集合Sub中的每一個(gè)組件都反常的情況下(相當(dāng)于指定Sub組件集合中的組件為診斷解,即加入單元子句,將其置為正文字),也就相當(dāng)于將組件集合Sub中的每一個(gè)組件所對(duì)應(yīng)的子句置為恒真子句,接著看剩余的組件集合(COMPS-Sub)都正常的情況下,是否能正常解釋系統(tǒng)在當(dāng)前觀測(cè)下面的行為(相應(yīng)的這3步對(duì)應(yīng)算法1的Step1,Step2,Step3).最后在Step4中調(diào)用SAT求解器,看看是否能解釋系統(tǒng)在當(dāng)前狀態(tài)下的行為,如果是可滿足的,返回1,表明能解釋,那么我們假設(shè)組件集合Sub為診斷解成立,Sub是系統(tǒng)的基于一致性診斷的解.如果是不可滿足的,返回0,那么表明在假設(shè)組件集合Sub為故障的情況下,不能解釋系統(tǒng)現(xiàn)在的行為,則Sub不是系統(tǒng)的基于一致性診斷的診斷解.

    ISDAG算法僅僅只能判斷一個(gè)組件集合是否是系統(tǒng)的診斷解,即只能得到系統(tǒng)的一個(gè)解,如果想要得到所有的診斷解,那么需要枚舉出所有的組件集合,然后對(duì)這些集合進(jìn)行判斷,進(jìn)一步得到所有解.

    2.2 利用枚舉樹求解所有診斷解

    為了求解給定診斷系統(tǒng)的所有基于一致性診斷的極小診斷解,我們只需要考慮所有可能出現(xiàn)故障的集合,假設(shè)該組件集合是故障組件集合,則調(diào)用算法ISDAG判斷該組件集合是不是診斷解.這個(gè)過(guò)程其實(shí)就是一個(gè)枚舉所有組件集合的過(guò)程,可以用枚舉樹來(lái)進(jìn)行枚舉,下面我們簡(jiǎn)單介紹一下枚舉樹.

    集合枚舉樹(set-enumeration-tree,SE-tree)是由國(guó)外學(xué)者Rymon[24]提出,這種樹模型在很大程度上可以枚舉出給定的集合中元素的所有可能的組合.例如當(dāng)前集合SS= {N1,N2,N3,N4},則集合SS的完全集合枚舉樹如圖3所示.

    根據(jù)圖3的樹模型,在求解系統(tǒng)的所有診斷的過(guò)程中,我們用這棵樹對(duì)求解過(guò)程進(jìn)行模擬.利用集合枚舉樹模型我們要求解所有的診斷解,只需要遍歷這棵樹上的所有結(jié)點(diǎn),對(duì)每個(gè)結(jié)點(diǎn)進(jìn)行相應(yīng)地判斷就可以得到最后的解.例如,針對(duì)集合{N2,N3},我們表示的是當(dāng)組件集合{N2,N3}都出現(xiàn)故障時(shí),組件N1,N4正常的情況下,是否能解釋系統(tǒng)當(dāng)前的行為.那么就需要調(diào)用ISDAG算法,將組件集合{N2,N3}作為輸入?yún)?shù),進(jìn)行判斷.如果調(diào)用ISDAG算法的返回值是1,那么表明組件集合{N2,N3}是系統(tǒng)的診斷解,如果是0,那么它就不是診斷解.當(dāng)然,為了求解所有的極小診斷解,我們只需要保留樹中其真子集不是診斷解的所有結(jié)點(diǎn),這些結(jié)點(diǎn)就是最后的基于一致性診斷的極小診斷解.

    Fig. 3 SE-tree of set SS圖3 集合SS的SE-tree

    近些年以來(lái),大部分求解系統(tǒng)的基于一致性診斷都是根據(jù)上面的枚舉樹,按照廣度優(yōu)先遍歷或者深度優(yōu)先遍歷,采用一定的剪枝規(guī)則,減少遍歷的結(jié)點(diǎn),從而得到最后的診斷解.

    趙相福等人[11-12]提出了CSSE-tree方法,CSSE-tree也是基于這樣的一棵枚舉樹,對(duì)整個(gè)枚舉樹中的結(jié)點(diǎn)進(jìn)行遍歷,然后進(jìn)行相應(yīng)的操作得到最后的極小診斷解.CSSE-tree的提出使得求解基于一致性診斷的求解時(shí)間得到了提升,它的優(yōu)點(diǎn)有2點(diǎn):

    1) 根據(jù)系統(tǒng)的組件個(gè)數(shù),系統(tǒng)地枚舉出跟該組件集合相關(guān)冪集的所有元素,然后從根結(jié)點(diǎn)開始進(jìn)行廣度優(yōu)先遍歷,這樣保證產(chǎn)生的解集是極小診斷解,并且保證了CSSE-tree的完備性,不會(huì)丟掉任何一個(gè)解.

    2) 根據(jù)極小診斷解的定義可以知道,一個(gè)極小診斷解的真超集一定不是極小診斷解.CSSE-tree利用該特征作為修剪規(guī)則,避免了所有極小診斷解真超集的判斷,而且由極小診斷解得定義保證了修剪規(guī)則的正確性.通過(guò)修剪規(guī)則可以減少一些不是極小診斷解的結(jié)點(diǎn)產(chǎn)生,使樹中的結(jié)點(diǎn)數(shù)目減少,從而使得求解的效率得到相應(yīng)的提高.

    然而CSSE-tree也存在2個(gè)缺點(diǎn):

    1) 如果系統(tǒng)的組件個(gè)數(shù)太多,枚舉出跟組件集合相關(guān)冪集合的所有元素將會(huì)使得CSSE-tree變得相當(dāng)?shù)谬嫶?,使得空間復(fù)雜度相當(dāng)?shù)么?而且,如果在解很少的情況下,修剪規(guī)則的剪枝空間較少,效率提升較小.

    2) 根據(jù)對(duì)實(shí)際例子的分析,我們知道枚舉樹中不是解的結(jié)點(diǎn)占據(jù)了枚舉樹中大量的結(jié)點(diǎn).CSSE-tree中的修剪規(guī)則只是對(duì)是解的那些結(jié)點(diǎn)起作用,對(duì)于不是解的那些結(jié)點(diǎn),只能進(jìn)行逐個(gè)判斷求解.

    根據(jù)上面對(duì)CSSE-tree方法的分析,我們可以知道,在求極小診斷解時(shí),是解的結(jié)點(diǎn)只是小部分,在我們判斷的過(guò)程中,不是診斷解的結(jié)點(diǎn)占據(jù)了樹中大量的結(jié)點(diǎn).不能對(duì)非解的結(jié)點(diǎn)進(jìn)行相應(yīng)地處理是CSSE-tree方法最致命的缺點(diǎn),如果能給出相應(yīng)的策略剪掉一些不是解的結(jié)點(diǎn),那么求解的效率將會(huì)得到進(jìn)一步的提高.基于剪掉不是解的結(jié)點(diǎn)這樣的思想,我們提出了基于反向搜索的有解無(wú)解剪枝方法,不僅剪掉是診斷解但非極小診斷解的一些結(jié)點(diǎn),而且剪掉樹中大部分不是解的結(jié)點(diǎn).

    3 基于反向搜索的有解無(wú)解空間剪枝方法

    2.2節(jié)描述了基于枚舉樹,結(jié)合ISDAG算法求診斷系統(tǒng)的所有基于一致性診斷的診斷解.然而我們發(fā)現(xiàn)枚舉樹中大量的結(jié)點(diǎn)都不是解,據(jù)此我們提出了基于反向搜索的有解無(wú)解剪枝方法.該方法不但可以剪掉是解但非極小診斷解的一些結(jié)點(diǎn),而且也剪掉了不是解的結(jié)點(diǎn),使得我們遍歷整棵枚舉樹的過(guò)程中,不用遍歷到所有的結(jié)點(diǎn),只需要遍歷少量的結(jié)點(diǎn),這樣可以加快求解所有解的過(guò)程.本節(jié)首先給出相關(guān)的一些定義,然后描述基于反向搜索的有解無(wú)解剪枝方法.

    3.1 有解剪枝和無(wú)解剪枝

    首先給出在這部分要用到的相關(guān)的定義:

    定義7. 有解剪枝.給定一棵枚舉樹,在遍歷這棵枚舉樹時(shí),對(duì)于樹中的某一個(gè)結(jié)點(diǎn),如果先判斷其父結(jié)點(diǎn)或者祖先結(jié)點(diǎn),得到的結(jié)果是可滿足的,那么該結(jié)點(diǎn)一定不是極小診斷解,可以不用對(duì)其進(jìn)行判斷.稱跳過(guò)枚舉樹中這樣結(jié)點(diǎn)的過(guò)程叫做有解剪枝.

    定義8. 無(wú)解剪枝.給定一棵枚舉樹,在遍歷這棵枚舉樹時(shí),對(duì)于樹中的某一個(gè)結(jié)點(diǎn),如果先判斷其子結(jié)點(diǎn)或者子孫結(jié)點(diǎn),得到的結(jié)果是不可滿足,那么可以跳過(guò)該結(jié)點(diǎn),不用對(duì)這個(gè)結(jié)點(diǎn)進(jìn)行判斷.我們稱跳過(guò)判斷枚舉樹中這樣結(jié)點(diǎn)的過(guò)程叫做無(wú)解剪枝.

    定義7和定義8是基于原理基于極小診斷的定義,即如果一個(gè)組件集合是極小診斷解,那么其真超集一定不是極小診斷解;如果一個(gè)組件集合不是診斷解,那么其真子集一定不是診斷解.

    定義9. 反向搜索.針對(duì)一棵枚舉樹,當(dāng)枚舉樹的層數(shù)已經(jīng)給定時(shí),稱從枚舉樹的最后一層向枚舉樹的根結(jié)點(diǎn)搜索的過(guò)程為樹的反向搜索.

    根據(jù)反向搜索的定義,只需要從樹的最后一層向根結(jié)點(diǎn)進(jìn)行向上搜索即可,在中間這些層之間,可以是自上向下,也可以是自下而上.并且,在訪問(wèn)中間層這些結(jié)點(diǎn)時(shí)并沒(méi)有固定的順序,只需要遍歷整棵樹的所有結(jié)點(diǎn)就可以.

    為了解釋上面的定義,我們舉例說(shuō)明,如S={N1,N2,N3,N4}的部分枚舉樹如圖4所示:

    Fig. 4 Part SE-tree of set S圖4 集合S的部分枚舉樹

    在這棵枚舉樹中,除了根結(jié)點(diǎn)以外,一共有14個(gè)結(jié)點(diǎn),為了得到所有的解,我們要遍歷樹上的所有結(jié)點(diǎn).對(duì)這棵樹進(jìn)行反向搜索時(shí),我們先遍歷最后一層的一些結(jié)點(diǎn),如{N1,N2,N3},{N1,N2,N4},然后遍歷第2層的結(jié)點(diǎn){N1,N2};接著再去遍歷第3層的結(jié)點(diǎn){N1,N3,N4}、第2層的結(jié)點(diǎn){N1,N3},{N1,N4}、第1層的結(jié)點(diǎn){N1}.根據(jù)這樣的遍歷方式,我們可以遍歷結(jié)點(diǎn){N2},{N3},{N4}這些結(jié)點(diǎn)以及這些結(jié)點(diǎn)的子孫結(jié)點(diǎn).

    在求診斷解的過(guò)程中,在進(jìn)行反向搜索時(shí),我們需要一邊遍歷結(jié)點(diǎn)、一邊對(duì)結(jié)點(diǎn)調(diào)用SAT求解器進(jìn)行判斷.在這個(gè)過(guò)程中,根據(jù)結(jié)點(diǎn)的判斷結(jié)果,可以知道樹中的某些結(jié)點(diǎn)可以不用遍歷,那么可以跳過(guò)樹中一些結(jié)點(diǎn)的判斷過(guò)程,減少調(diào)用SAT求解器的次數(shù),這就是剪枝過(guò)程.剪枝的過(guò)程可能是針對(duì)是解的那些結(jié)點(diǎn),也有可能是針對(duì)不是解的那些結(jié)點(diǎn),也就是有解剪枝和無(wú)解剪枝過(guò)程.例如,對(duì)于上面的這棵枚舉樹,我們基于反向搜索以及有解剪枝和無(wú)解剪枝的思想,求解極小診斷解的過(guò)程如下:

    針對(duì)上面的這棵枚舉樹,樹中一共有第1層的{N1},{N2},{N3},{N4}這4個(gè)結(jié)點(diǎn)以及它們的子樹構(gòu)成了這棵樹.對(duì)這4個(gè)結(jié)點(diǎn)處理的方式是一樣的,只對(duì)結(jié)點(diǎn){N1}進(jìn)行舉例說(shuō)明.針對(duì)結(jié)點(diǎn){N1}及其子孫結(jié)點(diǎn),我們首先判斷最后一層結(jié)點(diǎn){N1,N2,N3}的可滿足性,如果該結(jié)點(diǎn)是可滿足的,那么向上回溯,判斷{N1,N2}結(jié)點(diǎn).否則,根據(jù)無(wú)解剪枝的定義,可以剪掉結(jié)點(diǎn){N1,N2},接著繼續(xù)判斷結(jié)點(diǎn){N1,N2,N4}.如果{N1,N2,N3}可滿足,{N1,N2}也可滿足,那么根據(jù)有解剪枝的定義,可以剪掉結(jié)點(diǎn){N1,N2,N4},然后向上回溯判斷結(jié)點(diǎn){N1}.否則如果{N1,N2}不可滿足,那么結(jié)點(diǎn){N1}被剪掉,接著判斷{N1,N2,N4},然后是{N1,N3,N4}.如果結(jié)點(diǎn){N1,N2,N3},{N1,N2},{N1}都可滿足,那么根據(jù)有解剪枝的定義,結(jié)點(diǎn){N1}下面的所有其他結(jié)點(diǎn)都被剪掉,接著判斷以{N2}為根的子樹,判斷{N2,N3,N4}.否則如果{N1}不可滿足,那么我們接著判斷{N1,N3,N4}.到了判斷{N1,N3,N4}時(shí),我們按照判斷{N1,N2,N3}的模式繼續(xù)判斷即可.在存儲(chǔ)極小解的過(guò)程中,我們將可滿足的解存起來(lái),但是如果新來(lái)一個(gè)解,我們會(huì)判斷是否是已經(jīng)存在解的子集,如果是,那么將會(huì)更新原來(lái)的解,否則將新解加入到解集中.

    根據(jù)上面的求解思路,我們?cè)?.2節(jié)給出基于反向搜索的有解無(wú)解空間剪枝算法.

    3.2 基于反向搜索的有解無(wú)解空間剪枝算法

    基于有解剪枝和無(wú)解剪枝這樣的思想,我們可以從枚舉樹的第1層最左邊的第1棵子樹開始,對(duì)第1層的每個(gè)結(jié)點(diǎn)以及子樹按相同方式處理即可.針對(duì)每一棵子樹,我們先判斷其最左邊的結(jié)點(diǎn),如果是可滿足的,我們反向搜索,判斷其父結(jié)點(diǎn),并且將其根據(jù)有解剪枝的定義,將該結(jié)點(diǎn)還沒(méi)有訪問(wèn)的子孫結(jié)點(diǎn)都剪掉.如果是不可滿足,那么可以根據(jù)無(wú)解剪枝的定義,跳過(guò)對(duì)該節(jié)點(diǎn)父節(jié)點(diǎn)的遍歷,然后接著判斷該結(jié)點(diǎn)右邊的結(jié)點(diǎn).

    那么下面我們給出該算法的偽代碼:

    算法2. LLBRS-tree算法.

    輸入:系統(tǒng)描述的CNF文件DigSysDis.cnf、系統(tǒng)觀測(cè)的CNF文件DigSysObs.cnf、極小診斷的最大診斷長(zhǎng)度MiniDigLen;

    輸出:極小診斷解的集合.

    局部變量:診斷解集合DigRes[]、診斷系統(tǒng)組件的個(gè)數(shù)ComNum、枚舉樹的總層數(shù)DigTreeLevel、待判斷的第1層的某個(gè)結(jié)點(diǎn)及其子樹Sub-tree.

    Step1. 初始化:DigRes=?,ComNum=0,DigTreeLevel=0.

    Step2. 從文件DigSysDis.cnf中的第1行中讀取出診斷系統(tǒng)中組件的個(gè)數(shù),賦值給變量ComNum,然后根據(jù)輸入的最小診斷長(zhǎng)度MiniDigLen,賦值給變量DigTreeLevel.然后根據(jù)局部變量ComNum,DigTreeLevel的值,生成集合{1,2,3,…,ComNum}的局部集合枚舉樹DigSE-tree,DigTreeLevel是DigSE-tree的最大層數(shù)(根結(jié)點(diǎn)默認(rèn)為第0層).

    Step3. 將DigSE-tree的第1層最左邊的結(jié)點(diǎn)及其子樹賦值給Sub-tree.

    Step4. while(DigSE-tree中存在第1層結(jié)點(diǎn)及其子樹還沒(méi)判斷).

    Step4.1. while(Sub-tree判斷未完成)

    對(duì)該子樹最底層的最左邊的結(jié)點(diǎn)調(diào)用ISDAG算法判斷;

    if (該結(jié)點(diǎn)可滿足)

    ① 將該結(jié)點(diǎn)加入到診斷解結(jié)合DigRes中,并且將在DigRes中所有該結(jié)點(diǎn)的真超集刪除;

    ② 有解剪枝,將該結(jié)點(diǎn)的沒(méi)有訪問(wèn)過(guò)的子孫結(jié)點(diǎn)剪掉;

    ③ 對(duì)該結(jié)點(diǎn)的父結(jié)點(diǎn)進(jìn)行判斷;

    else

    ① 無(wú)解剪枝,將該結(jié)點(diǎn)的父結(jié)點(diǎn)剪掉;

    ② 對(duì)該結(jié)點(diǎn)的右邊的結(jié)點(diǎn)進(jìn)行判斷;

    end if

    Step4.2. 將第1層的下一個(gè)結(jié)點(diǎn)及其子樹賦值給Sub-tree,接著對(duì)Sub-tree進(jìn)行判斷.

    Step5. 返回集合DigRes.

    1) 該算法是完備的,會(huì)得到所有的極小診斷解,不會(huì)出現(xiàn)丟掉一部分解的情況.因?yàn)槲覀冇靡豢妹杜e樹的形式將所有可能出現(xiàn)的情況都一一列舉出來(lái),所以不會(huì)出現(xiàn)丟解,所有的極小診斷解在遍歷完這棵樹以后全部產(chǎn)生.

    2) 通過(guò)對(duì)第2節(jié)的ISDAG算法分析可以發(fā)現(xiàn),在ISDAG算法中的Step2這一步,當(dāng)我們向系統(tǒng)描述文件DigSysDis.cnf中添加的反常單元子句的數(shù)目越多時(shí),那么意味著單元傳播的次數(shù)將會(huì)很多,文件DigSysDis.cnf中可滿足的子句數(shù)目也會(huì)大大地增加,繼而調(diào)用SAT求解器對(duì)該文件進(jìn)行可滿足性判斷的時(shí)間也將會(huì)相應(yīng)地縮短.在LLBRS-tree算法中,我們先對(duì)長(zhǎng)度長(zhǎng)的結(jié)點(diǎn)進(jìn)行判斷,這些結(jié)點(diǎn)的長(zhǎng)度與極小診斷解的最大長(zhǎng)度相等,那么相應(yīng)地在調(diào)用ISDAG算法時(shí),使得在調(diào)用SAT求解器對(duì)DigSysDis.cnf文件處理的時(shí)間縮短.同時(shí),先對(duì)長(zhǎng)度最長(zhǎng)的結(jié)點(diǎn)進(jìn)行處理,那么我們可以進(jìn)行無(wú)解剪枝的過(guò)程,這樣在反向搜索向上判斷時(shí)可以剪掉大量不是診斷解的結(jié)點(diǎn).所以,利用LLBRS-tree算法去求解給定系統(tǒng)的基于一致性診斷的極小診斷時(shí),時(shí)間效率將會(huì)得到大大地提高.

    3) 算法LLBRS-tree的時(shí)間復(fù)雜度以及空間復(fù)雜度主要取決于樹中遍歷的結(jié)點(diǎn)數(shù)目.在生成該樹時(shí),我們可以用自動(dòng)機(jī)去模擬樹中結(jié)點(diǎn)的生成,并且隨著結(jié)點(diǎn)的生成與判斷,樹中的大量結(jié)點(diǎn)都會(huì)被有解剪枝和無(wú)解剪枝剪掉,從而調(diào)用SAT的次數(shù)也是大大地減少.當(dāng)我們?cè)谔幚斫M件個(gè)數(shù)不是很多,且求解的是單雙診斷時(shí),效率可能不是很明顯.但是當(dāng)組件個(gè)數(shù)很多時(shí),無(wú)解剪枝將會(huì)剪掉大量的結(jié)點(diǎn),求解的時(shí)間將會(huì)得到大大地縮短.

    4 實(shí)驗(yàn)結(jié)果

    本節(jié)我們對(duì)趙相福等人提出的CSSE-trees算法和本文提出的LLBRS-tree算法進(jìn)行了實(shí)現(xiàn),同時(shí)將2個(gè)算法進(jìn)行多方面地比較.測(cè)試環(huán)境為:Dell Dimension C521,Ubuntu 12.04 LTS,GCC編譯器,AMD AthlonTM64 X2 Dual Core Processor 3600+,1.90 GHz,3 GB RAM.其中在算法ISDAG中,我們調(diào)用的SAT求解器是Picosat[25],該求解器在SAT比賽中也取得了不錯(cuò)的成績(jī),而且該求解器的接口寫得很詳細(xì),在使用接口時(shí)很方便,所以我們選擇了該求解器.

    我們使用的測(cè)試用例均來(lái)自于基準(zhǔn)電路ISCAS-85[26]中7個(gè)電路,它們分別是c17,c432,c499,c880,c1355,c2670,c3540.我們首先通過(guò)這些電路的電路描述得到各個(gè)電路的系統(tǒng)描述文件DigSysDis.cnf,然后根據(jù)給出的觀測(cè)值得到系統(tǒng)的觀測(cè)文件DigSysObs.cnf,這些CNF形式的文件都是離線構(gòu)造.然后我們分別使用CSSE-tree算法和LLBRS-tree算法對(duì)ISCAS-85的這幾個(gè)電路進(jìn)行多次測(cè)試,記錄了相關(guān)的求解時(shí)間.我們分別用2種算法對(duì)這些電路求解長(zhǎng)度為1,2,3的極小診斷,得到的結(jié)果如表1所示:

    Table 1 Solution Time

    ×:Timeout.

    從表1中可以看出,在極小診斷解得最大長(zhǎng)度為1時(shí),算法LLBRS-tree跟算法CSSE-tree的求解時(shí)間基本持平,“×”表示在1 h內(nèi)求解失敗.這是因?yàn)楫?dāng)極小診斷解的最大長(zhǎng)度為1時(shí),2個(gè)算法都需要遍歷枚舉樹中的所有結(jié)點(diǎn),沒(méi)有剪枝的情況,所以2個(gè)算法的時(shí)間基本一樣.但是當(dāng)極小診斷解的最大長(zhǎng)度為2和3時(shí),算法LLBRS-tree的求解時(shí)間比算法CSSE-tree的時(shí)間少了很多.算法LLBRS-tree的時(shí)間在平均情況下提高了5%左右,而且在極小診斷解的最大長(zhǎng)度為3時(shí),有些例子可以達(dá)到8%.這是因?yàn)殡S著極小診斷解的最大長(zhǎng)度的增加,枚舉樹的層數(shù)相應(yīng)地增加,樹中結(jié)點(diǎn)的數(shù)目也增加,那么樹中不是解的結(jié)點(diǎn)個(gè)數(shù)多于是解的結(jié)點(diǎn)個(gè)數(shù).在這樣的情況下,LLBRS-tree算法將會(huì)對(duì)枚舉樹進(jìn)行無(wú)解剪枝和有解剪枝,遍歷求解的結(jié)點(diǎn)數(shù)也將少于CSSE-tree算法,所以效率得到了提高.為了說(shuō)明LLBRS-tree算法遍歷的結(jié)點(diǎn)數(shù)目小于CSSE-tree算法遍歷的結(jié)點(diǎn)數(shù)目,我們給出2個(gè)算法剪掉的結(jié)點(diǎn)個(gè)數(shù),如表2所示.

    由于單診斷并沒(méi)有涉及到有解剪枝和無(wú)解剪枝的情況,所以我們?cè)诒?中只給出了2診斷和3診斷的結(jié)點(diǎn)剪枝情況,“×”表示在1 h內(nèi)求解失敗.而且針對(duì)c1908,c2670,c3540這3個(gè)電路,我們?cè)O(shè)置的求解時(shí)間限制是10 000 s,但是由于這3個(gè)電路的組件個(gè)數(shù)過(guò)多,所以2個(gè)算法都超出了時(shí)間的限制.根據(jù)表2中的雙診斷剪枝結(jié)點(diǎn)的信息,由Δ這一列的差值信息Δ=(LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)-CSSE-tree剪掉的結(jié)點(diǎn)數(shù))可以看出,由于存在無(wú)解剪枝的情況,而且伴隨著有解剪枝,LLBRS-tree算法剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)多于CSSE-tree算法剪掉的結(jié)點(diǎn)數(shù)目.而且當(dāng)我們求解3診斷時(shí),枚舉樹中的結(jié)點(diǎn)數(shù)目急劇增加,算法LLBRS-tree的作用更加地顯現(xiàn)出來(lái).從3診斷的Δ那一列數(shù)據(jù),我們看出:算法LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)遠(yuǎn)遠(yuǎn)大于算法CSSE-tree剪掉的結(jié)點(diǎn)數(shù)目,有的例子剪掉的結(jié)點(diǎn)數(shù)目已經(jīng)高出CSSE-tree算法的十幾倍.這是因?yàn)椋S著枚舉樹的層數(shù)增加,樹中不可滿足的結(jié)點(diǎn)數(shù)目也大大地增加了,那么算法LLBRS-tree的無(wú)解剪枝策略將會(huì)發(fā)揮關(guān)鍵的作用,所以剪掉的結(jié)點(diǎn)數(shù)目遠(yuǎn)遠(yuǎn)大于算法CSSE-tree.基于這樣的原因,算法LLBRS-tree在求解的過(guò)程中所消耗的時(shí)間才會(huì)小于CSSE-tree算法.而且,隨著枚舉樹的層數(shù)增加,也就是當(dāng)極小診斷解的最大長(zhǎng)度增加時(shí),樹中不是解的結(jié)點(diǎn)數(shù)目還會(huì)不斷地增加,遠(yuǎn)遠(yuǎn)大于是解的結(jié)點(diǎn)數(shù)目,那么算法LLBRS-tree的無(wú)解剪枝剪掉的結(jié)點(diǎn)也將會(huì)大幅度地增加,該算法的效率也會(huì)彰顯出來(lái),而CSSE-tree算法的效率將會(huì)變得越來(lái)越慢,更有可能內(nèi)存溢出的情況.我們分別用2種算法針對(duì)組件個(gè)數(shù)適中的幾個(gè)測(cè)試用例求解多診斷得到的結(jié)果如表3所示.

    Table 2 Numbers of Cut Node

    ×: Timeout.

    Table 3 Time of Multi-Diagnosis

    M.O: Out of memory.

    從表3中可以看出,在求解多診斷時(shí),算法LLBRS-tree的求解時(shí)間遠(yuǎn)遠(yuǎn)小于算法CSSE-tree.測(cè)試用例為c432并且診斷長(zhǎng)度為4時(shí),算法CSSE-tree求解時(shí)間是算法LLBRS-tree的2.6倍;但是當(dāng)求解5診斷時(shí),卻是3.3倍;并且當(dāng)診斷長(zhǎng)度為6時(shí),CSSE-tree算法出現(xiàn)了內(nèi)存溢出的情況,而算法LLBRS-tree仍然能求解.當(dāng)測(cè)試用例為c499和c880時(shí),伴隨著組件個(gè)數(shù)和診斷長(zhǎng)度的增加,算法CSSE-tree更早的出現(xiàn)了內(nèi)存溢出的情況,而算法LLBRS依舊能正常的工作.這是因?yàn)樗惴↙LBRS-tree針對(duì)無(wú)解剪枝空間進(jìn)行大量剪枝,加上有解空間的剪枝,使得需要判斷的結(jié)點(diǎn)很少.而算法LLBRS生成大量的結(jié)點(diǎn)進(jìn)行判斷,導(dǎo)致了內(nèi)存溢出.重要的是,根據(jù)LLBRS-tree算法的求解時(shí)間我們可以發(fā)現(xiàn),即使診斷長(zhǎng)度增加,該算法的求解時(shí)間也是平緩的增加,不會(huì)出現(xiàn)劇烈的抖動(dòng).這是由于有解無(wú)解剪枝策略在求解過(guò)程中起到重要的作用.為了更加清晰地說(shuō)明這種情況,我們對(duì)測(cè)試用例c432求多診斷得到結(jié)果如圖5所示:

    Fig. 5 Comparison chart of multi-diagnosis (ISCAS-85_c432)圖5 多診斷時(shí)間對(duì)比圖(ISCAS-85_c432)

    圖5是算法LLBRS-tree和算法CSSE-tree針對(duì)電路c432(160個(gè)組件)求解診斷1~10的時(shí)間對(duì)比圖.從圖5我們可以看出,在求解3診斷以前,2個(gè)算法的時(shí)間相差幾乎沒(méi)有太大的差距.但是在求解4~5診斷時(shí),從2條線的斜率可以看出,算法LLBRS-tree的時(shí)間增加很平緩,而CSSE-tree算法求解的時(shí)間急劇增加.而且更重要的是,算法LLBRS-tree在求解6~10診斷時(shí),時(shí)間依舊很平緩地增加,不會(huì)出現(xiàn)急劇增加的情況,但是算法CSSE-tree卻只能求到5診斷,6~10診斷出現(xiàn)了內(nèi)存溢出的情況,不能求出結(jié)果.這是因?yàn)闃渲薪Y(jié)點(diǎn)的數(shù)目急劇地增加,算法CSSE-tree剪掉的結(jié)點(diǎn)很少,隨著結(jié)點(diǎn)的膨脹,所以算法出現(xiàn)了內(nèi)存溢出的情況.而算法LLBRS-tree進(jìn)行無(wú)解剪枝,剪掉大量不是解的結(jié)點(diǎn),所以針對(duì)多診斷,依舊能正常地運(yùn)行.

    由上面的實(shí)驗(yàn)結(jié)果可以知道,對(duì)于沒(méi)有應(yīng)用無(wú)解空間剪枝策略的求解算法,當(dāng)組件集合增加,極小診斷長(zhǎng)度加大,并且診斷解分布在集合枚舉樹的右側(cè)時(shí),算法的時(shí)間復(fù)雜性是指數(shù)級(jí).但是應(yīng)用本文提出的有解和無(wú)解剪枝策略后,樹中不是診斷解的結(jié)點(diǎn)將會(huì)被減掉大部分,算法的時(shí)間復(fù)雜度將小于指數(shù)級(jí).由于受到具體診斷實(shí)例的輸入和輸出觀測(cè)影響,基于模型診斷算法的時(shí)間復(fù)雜度將會(huì)變得十分復(fù)雜,這也將成為我們以后研究工作的一部分.

    5 結(jié)束語(yǔ)

    基于模型診斷在人工智能領(lǐng)域一直以來(lái)都備受關(guān)注,從問(wèn)題的提出到現(xiàn)在,越來(lái)越多的人投入到該問(wèn)題的研究中.基于極小診斷解的真超集一定不是極小診斷解的原理,CSSE-tree對(duì)枚舉樹進(jìn)行了修剪,提高了診斷求解效率.但是CSSE-tree只是針對(duì)是解的結(jié)點(diǎn)進(jìn)行剪枝,并沒(méi)有考慮不是解的結(jié)點(diǎn).本文首次提出對(duì)無(wú)解進(jìn)行剪枝的思想,并結(jié)合有解剪枝給出LLBRS-tree診斷求解方法.

    在LLBRS-tree算法中,根據(jù)包含組件個(gè)數(shù)較多的候選診斷解對(duì)應(yīng)的SAT問(wèn)題規(guī)模較小的特點(diǎn),先對(duì)包含組件個(gè)數(shù)較多的結(jié)點(diǎn)進(jìn)行判斷,進(jìn)而從減少求解問(wèn)題規(guī)模的角度提高診斷求解效率.算法LLBRS-tree剪掉的結(jié)點(diǎn)數(shù)目遠(yuǎn)大于算法CSSE-tree,所以求解所用的時(shí)間更短,效率高于算法CSSE-tree.尤其在求解多診斷時(shí),所要枚舉結(jié)點(diǎn)的數(shù)目急劇增加,算法CSSE-tree只對(duì)有解進(jìn)行剪枝,剪掉的結(jié)點(diǎn)較少.而算法LLBRS-tree進(jìn)行無(wú)解和有解剪枝,在剪掉有解空間基礎(chǔ)上還剪掉大量不是解的結(jié)點(diǎn).所以,在求解多診斷時(shí),算法LLBRS-tree剪掉的結(jié)點(diǎn)更多,與算法CSSE-tree相比,效率有更大提高.

    在后續(xù)的工作中,我們考慮利用增量SAT求解器來(lái)求解基于模型的診斷,只需要一次調(diào)用SAT求解器,就可以得到多個(gè)解,這樣求解效率會(huì)得到進(jìn)一步提升.

    [1]Raymond R. A theory of diagnosis from first principles[J]. Artificial Intelligence, 1987, 32(1): 57-95

    [2]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal hitting sets based on join relation[J].IEEE Trans on Systems Man Cybernetics-Systems, 2015, 45(7): 1063-1076

    [3]Jiang Yunfei, Lin Li. The computation of hitting sets with boolean formulas[J]. Chinese Journal of Computers, 2003, 26(8): 919-924 (in Chinese)(姜云飛, 林笠. 用布爾代數(shù)方法計(jì)算最小碰集[J].計(jì)算機(jī)學(xué)報(bào), 2003, 26(8): 919-924)

    [4]Zhang Liming, Ouyang Dantong, Zeng Hailin. Computing the minimal hitting set based on dynamic maximum degree[J]. Journal of Computer Research and Development, 2011, 48(2): 209-215 (in Chinese) (張立明, 歐陽(yáng)丹彤, 曾海林. 基于動(dòng)態(tài)極大度的極小碰集求解方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2011, 48(2): 209-215)

    [5]Wang Yiyuan, Ouyang Dantong, Zhang Liming, et al. A method of computing minimal hitting sets using CSP[J]. Journal of Computer Research and Development, 2015, 52(3): 588-595 (in Chinese) (王藝源, 歐陽(yáng)丹彤, 張立明,等. 利用CSP求解極小碰集的方法[J]. 計(jì)算機(jī)研究與發(fā)展, 2015, 52(3): 588-595)

    [6]Huang Jie, Chen Lin, Zou Peng. Computing minimal diagnosis by compounded genetic and simulated annealing algorithm[J]. Journal of Software, 2004, 15(9): 1345-1350 (in Chinese)(黃杰, 陳琳, 鄒鵬. 一種求解極小碰集的遺傳模擬退火算法[J]. 軟件學(xué)報(bào), 2004, 15(9): 1345-1350)

    [7]Liu Juan, Ouyang Dantong, Wang Yiyuan, et all. Computing minimal hitting sets with particle swarm optimization combined characteristics learning[J]. Acta Electronica Sinica, 2015, 43(5): 841-845 (in Chinese) (劉娟, 歐陽(yáng)丹彤, 王藝源, 等. 結(jié)合特征學(xué)習(xí)的粒子群求解極小碰集方法[J]. 電子學(xué)報(bào), 2015, 43(5): 841-845)

    [8]Chen Yunji, Zhang Jian, Shen Haihua. A SAT-Based arithmetic circuit bug-hunting method[J]. Chinese Journal of Computers, 2007, 30(12): 2082-2089 (in Chinese) (陳云霽, 張健, 沈海華. 一種基于 SAT 的運(yùn)算電路查錯(cuò)方法[J]. 計(jì)算機(jī)學(xué)報(bào), 2007, 30(12): 2082-2089)

    [9]Zhang Jian, Ma Feifei, Zhang Zhiqiang. Faulty interaction identification via constraint solving and optimization[G]Theory and Applications of Satisfiability Testing-SAT. Berlin: Springer, 2012: 186-199

    [10]Zhang Xuenong, Jiang Yunfei, Chen Aixiang, et al. A gradual approach for model-based diagnosis[J]. Journal of Software, 2008, 19(3): 584-593 (in Chinese) (張學(xué)農(nóng), 姜云飛, 陳藹祥,等. 基于模型診斷的分步求解[J]. 軟件學(xué)報(bào), 2008, 19(3): 584-593)

    [11]Zhao Xiangfu, Zhang Liming, Ouyang Dantong, et al. Deriving all minimal consistency-based diagnosis sets using SAT solvers[J]. Progress in Natural Science, 2009, 19(4): 489-494

    [12]Zhao Xiangfu, Ouyang Dantong. Deriving all minimal conflict sets using satisfiability algorithms[J]. Acta Electronica Sinica, 2009, 37(4): 804-810 (in Chinese) (趙相福, 歐陽(yáng)丹彤. 使用SAT求解器產(chǎn)生所有極小沖突部件集[J]. 電子學(xué)報(bào), 2009, 37(4): 804-810)

    [13]Zhang Liming, Zeng Hailin, Yang Fang, et al. Dynamic theorem proving algorithm for consistency-based diagnosis[J]. Expert Systems With Applications, 2011, 38(6): 7511-7516

    [14]Chen Rong, Gao Jian, Zhang Weishi. Digital circuit fault diagnosis method and system based on logic compatibility [P]. Chinese: CN102156772A, 2011-08-17 (in Chinese)(陳榮, 高健, 張維石. 基于邏輯相容性的數(shù)字電路故障診斷方法及系統(tǒng)[P]. 中國(guó): CN102156772A, 2011-08-17)

    [15]Ouyang Dantong, Zhang Liming, Zhao Jian. Solving model-based fault diagnosis with flag propagation[J]. Chinese Journal of Scientific Instrument, 2011, 32(12): 2857-2862 (in Chinese) (歐陽(yáng)丹彤, 張立明, 趙劍. 利用標(biāo)志傳播求解基于模型的故障診斷[J]. 儀器儀表學(xué)報(bào), 2011, 32(12): 2857-2862)

    [16]Luan Shangmin, Dai Guozhong. An approach to diagnosing a system with structure information[J]. Chinese Journal of Computers, 2005, 28(5): 801-808 (in Chinese)(欒尚敏, 戴國(guó)忠. 利用結(jié)構(gòu)信息的故障診斷方法[J]. 計(jì)算機(jī)學(xué)報(bào), 2005, 28(5): 801-808)

    [17]Xu Ke, Boussemart F, Hemery F, et al. Random constraint satisfaction: Easy generation of hard (satisfiable) instances[J]. Artificial Intelligence, 2007, 171(8): 514-534

    [18]Xu Ke, Li Wei. Exact phase transitions in random constraint satisfaction problems[J]. Journal of Artificial Intelligence Research, 2000, 12(1): 93-103

    [19]Zhou Junping, Yin Minghao, Zhou Chunguang, New worst-case upper bound for #2-SAT and #3-SAT with the number of clauses as parameter[C]Proc of the 24th AAAI Conf on Artificial Intelligence. Menlo Park: AAAI, 2010: 217-222

    [20] Luo Chuan, Cai Shaowei, Wu Wei, et al. Double configuration checking in stochastic local search for satisfiability[C]Proc of the 28th AAAI Conf on Artificial Intelligence. Menlo Park: AAAI, 2014: 2703-2709

    [21]Cai Shaowei, Su Kaile. Comprehensive score: Towards efficient local search for SAT with long clauses[C]Proc of the 23rd Int Joint Conf on Artificial Int. Menlo Park: AAAI, 2013: 489-495

    [22]Cai Shaowei, Su Kaile. Local search for Boolean Satisfiability with configuration checking and subscore[J]. Artificial Intelligence, 2013, 204(9): 75-98

    [23]Cai Dunbo, Yin Minghao. On the utility of landmarks in SAT based planning[J]. Knowledge-Based Systems, 2012, 36(6): 146-154

    [24]Rymon R. Search through systematic set enumeration[C]Proc of the 3rd Int conf on Principles of Knowledge Representation and Reasoning. San Franasco: Morgan Kaufmann, 1992: 539-550

    [25]Biere A. PicoSAT essentials[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2008, 4(20): 75-97

    [26]Metodi A, Stern R, Kalech M, et al. A novel SAT-based approach to model based diagnosis[J]. Journal of Artificial Intelligence Research, 2014, 51(1): 377-411

    Ouyang Dantong, born in 1968. Professor and PhD supervisor of Jilin University. Senior member of CCF. Her main research interests include model-based diagnosis, model checking and automated reasoning (ouyangdantong@163.com).

    Zhou Jianhua, born in 1991. Master candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning.

    Liu Bowen, born in 1993. Master candidate at Jilin University. His main research interests include model-based diagnosis, SAT problem and automated reasoning (1591365445@qq.com).

    Zhang Liming, born in 1980. PhD, Post-doctor in Jilin University. His main research interests include model-based diagnosis, model checking and Boolean satisfiability.

    A New Algorithm Combining with the Characteristic of the Problem for Model-Based Diagnosis

    Ouyang Dantong1,2,3, Zhou Jianhua1,3, Liu Bowen2,3, and Zhang Liming1,2,3

    1(CollegeofSoftware,JilinUniversity,Changchun130012)2(CollegeofComputerScienceandTechnology,JilinUniversity,Changchun130012)3(KeyLaboratoryofSymbolicComputationandKnowledgeEngineering(JilinUniversity),MinistryofEducation,Changchun130012)

    Model-based diagnosis has been popular in the field of artificial intelligence. In recent years, with a gradual increase of the efficiency of SAT solvers, model-based diagnosis is converted into SAT problem. After deeply studying CSSE-tree algorithm—a method for solving model-based diagnosis, combining with the characteristics of diagnose problem and SAT solving process, we solve the problem by diagnosing the candidate solutions which contain more elements first, thereby reducing the scale of SAT problem. Based on the minimal diagnostic solutions and non-minimal pruning methods on diagnostic solutions, we firstly propose a non-diagnostic solution theorem and a non-solution space pruning algorithm, which implements the non-solution space pruning effectively. We first solve the candidate solutions which contain more elements. According to the features of solution and non-solution method, we construct LLBRS-tree method based on reverse search. Experimental results show that compared with the algorithm of CSSE-tree, the algorithm of LLBRS-tree has less number of SAT solving, has smaller scale of the problem, better efficiency, especially when solving multiple diagnose problems its efficiency is more significant.

    model-based diagnosis; non-solution space pruning; conjunctive normal form; SAT solver; set-enumeration-tree

    2015-11-03;

    2016-04-13

    國(guó)家自然科學(xué)基金項(xiàng)目(61672261,61502199,61402196,61272208);浙江省自然科學(xué)基金項(xiàng)目(LY16F020004) This work was supported by the National Natural Science Foundation of China (61672261, 61502199, 61402196, 61272208) and the Natural Science Foundation of Zhejiang Province of China (LY16F020004).

    張立明(limingzhang@jlu.edu.cn)

    TP18

    猜你喜歡
    枚舉子句診斷系統(tǒng)
    命題邏輯中一類擴(kuò)展子句消去方法
    基于理解性教學(xué)的信息技術(shù)教學(xué)案例研究
    速讀·上旬(2022年2期)2022-04-10 16:42:14
    一種高效的概率圖上Top-K極大團(tuán)枚舉算法
    命題邏輯可滿足性問(wèn)題求解器的新型預(yù)處理子句消去方法
    區(qū)間軌道電路智能診斷系統(tǒng)的探討
    設(shè)備在線診斷系統(tǒng)在唐鋼的建設(shè)與應(yīng)用
    西夏語(yǔ)的副詞子句
    西夏學(xué)(2018年2期)2018-05-15 11:24:42
    基于太陽(yáng)影子定位枚舉法模型的研究
    命題邏輯的子句集中文字的分類
    連鑄板坯質(zhì)量在線診斷系統(tǒng)的應(yīng)用
    新疆鋼鐵(2015年2期)2015-11-07 03:27:52
    欧美一区二区国产精品久久精品| 3wmmmm亚洲av在线观看| 国产精品一区二区三区四区久久| 欧美一区二区亚洲| 男人的好看免费观看在线视频| 国产精品美女特级片免费视频播放器| 国产 一区 欧美 日韩| 国产亚洲精品久久久com| 在线观看日韩欧美| 免费一级毛片在线播放高清视频| 亚洲国产高清在线一区二区三| 每晚都被弄得嗷嗷叫到高潮| 99久久精品热视频| 少妇裸体淫交视频免费看高清| 18禁裸乳无遮挡免费网站照片| tocl精华| 尤物成人国产欧美一区二区三区| 亚洲一区二区三区不卡视频| ponron亚洲| 高清日韩中文字幕在线| 欧美性感艳星| e午夜精品久久久久久久| 男女那种视频在线观看| 国产乱人伦免费视频| 久久久久久九九精品二区国产| 亚洲精品成人久久久久久| 精品乱码久久久久久99久播| 香蕉丝袜av| 一个人观看的视频www高清免费观看| 黄色片一级片一级黄色片| www.熟女人妻精品国产| 国产精品98久久久久久宅男小说| 国内揄拍国产精品人妻在线| 99国产精品一区二区蜜桃av| 首页视频小说图片口味搜索| 国产熟女xx| 午夜福利在线在线| 亚洲av电影在线进入| 99riav亚洲国产免费| 久久草成人影院| 亚洲国产日韩欧美精品在线观看 | 国产精品一区二区三区四区久久| 18禁裸乳无遮挡免费网站照片| 久久久国产成人精品二区| 美女被艹到高潮喷水动态| 国产老妇女一区| 九九久久精品国产亚洲av麻豆| 久久久国产精品麻豆| 久久九九热精品免费| 欧美极品一区二区三区四区| 香蕉久久夜色| 欧美bdsm另类| 欧美黑人巨大hd| 色视频www国产| 亚洲国产欧美网| 大型黄色视频在线免费观看| 国产精品一区二区三区四区久久| 色精品久久人妻99蜜桃| 特大巨黑吊av在线直播| 观看免费一级毛片| 国产爱豆传媒在线观看| 国产欧美日韩精品亚洲av| 99国产精品一区二区蜜桃av| 国产精品 欧美亚洲| av专区在线播放| 一区二区三区高清视频在线| 一二三四社区在线视频社区8| 午夜亚洲福利在线播放| 国产单亲对白刺激| 久久久久免费精品人妻一区二区| 波多野结衣高清无吗| 精品国产美女av久久久久小说| 精品免费久久久久久久清纯| 婷婷丁香在线五月| 欧美日韩精品网址| 国产免费av片在线观看野外av| 日韩欧美免费精品| 在线看三级毛片| 国产色婷婷99| 国产精品国产高清国产av| 国产精品99久久久久久久久| 亚洲国产精品合色在线| 国内精品一区二区在线观看| 黄色日韩在线| 久久精品91蜜桃| 日韩中文字幕欧美一区二区| 中文字幕高清在线视频| 欧美一级a爱片免费观看看| 九色国产91popny在线| av黄色大香蕉| 美女被艹到高潮喷水动态| 啦啦啦观看免费观看视频高清| 久久久久精品国产欧美久久久| 最近最新中文字幕大全电影3| 国产高清videossex| 午夜福利成人在线免费观看| 看免费av毛片| 亚洲精品亚洲一区二区| 久久中文看片网| 最后的刺客免费高清国语| 人妻久久中文字幕网| 老司机深夜福利视频在线观看| 伊人久久大香线蕉亚洲五| 亚洲精品色激情综合| 男女下面进入的视频免费午夜| av片东京热男人的天堂| 欧美色视频一区免费| 久久6这里有精品| 男人的好看免费观看在线视频| 欧美成狂野欧美在线观看| 久久久国产成人免费| 非洲黑人性xxxx精品又粗又长| 精品熟女少妇八av免费久了| 三级毛片av免费| 亚洲国产精品久久男人天堂| 淫妇啪啪啪对白视频| 看免费av毛片| 日韩国内少妇激情av| 欧美一区二区精品小视频在线| eeuss影院久久| 欧美性感艳星| 国产成人av教育| 高潮久久久久久久久久久不卡| 久久精品国产综合久久久| 欧美日韩综合久久久久久 | 日本与韩国留学比较| 亚洲美女黄片视频| 琪琪午夜伦伦电影理论片6080| 欧美日韩乱码在线| 最近最新中文字幕大全免费视频| 美女cb高潮喷水在线观看| 欧美乱妇无乱码| 成人亚洲精品av一区二区| 啦啦啦韩国在线观看视频| 少妇高潮的动态图| 亚洲国产精品sss在线观看| www.999成人在线观看| 国产精品久久久久久人妻精品电影| 精品一区二区三区视频在线 | 免费在线观看日本一区| 国产精品国产高清国产av| 99国产极品粉嫩在线观看| 国产欧美日韩一区二区三| 观看美女的网站| 成人av在线播放网站| 国产欧美日韩一区二区精品| 一本久久中文字幕| 少妇的丰满在线观看| xxx96com| av天堂中文字幕网| 久久久成人免费电影| 国产精品自产拍在线观看55亚洲| 欧美黑人巨大hd| 18禁黄网站禁片午夜丰满| 欧美国产日韩亚洲一区| 小蜜桃在线观看免费完整版高清| 一个人看的www免费观看视频| 国内少妇人妻偷人精品xxx网站| 村上凉子中文字幕在线| 久久久成人免费电影| 免费看美女性在线毛片视频| 午夜精品久久久久久毛片777| 一卡2卡三卡四卡精品乱码亚洲| 免费av观看视频| 动漫黄色视频在线观看| 国产一区二区在线观看日韩 | 亚洲av熟女| 国产精品美女特级片免费视频播放器| 欧美大码av| 免费av不卡在线播放| 国产精品一区二区三区四区免费观看 | 天堂√8在线中文| 18禁在线播放成人免费| 18禁国产床啪视频网站| 亚洲乱码一区二区免费版| 久久国产乱子伦精品免费另类| 丁香欧美五月| 天天躁日日操中文字幕| www国产在线视频色| 窝窝影院91人妻| 亚洲久久久久久中文字幕| 欧美黑人欧美精品刺激| 国产精品一区二区三区四区久久| 五月玫瑰六月丁香| 亚洲熟妇中文字幕五十中出| 九色成人免费人妻av| 狠狠狠狠99中文字幕| 久久99热这里只有精品18| 波多野结衣高清无吗| 久久久久久九九精品二区国产| 熟女电影av网| 我的老师免费观看完整版| 一进一出抽搐gif免费好疼| 一区福利在线观看| 一本久久中文字幕| 午夜日韩欧美国产| 久久国产乱子伦精品免费另类| 国产精品三级大全| 少妇裸体淫交视频免费看高清| 免费看日本二区| 国产伦一二天堂av在线观看| 一区福利在线观看| 亚洲av免费高清在线观看| a级一级毛片免费在线观看| 午夜福利在线观看免费完整高清在 | 丰满的人妻完整版| 成人av在线播放网站| 午夜精品一区二区三区免费看| 一进一出抽搐gif免费好疼| 国产成人福利小说| 欧美成人免费av一区二区三区| 少妇高潮的动态图| 丰满人妻一区二区三区视频av | 性色avwww在线观看| 国产精品 国内视频| 老司机午夜福利在线观看视频| 亚洲第一电影网av| 12—13女人毛片做爰片一| 人妻夜夜爽99麻豆av| 免费高清视频大片| 免费在线观看成人毛片| 欧美激情久久久久久爽电影| 男女午夜视频在线观看| 制服丝袜大香蕉在线| 人妻久久中文字幕网| 欧美乱码精品一区二区三区| 亚洲精品在线观看二区| 美女cb高潮喷水在线观看| 国产在线精品亚洲第一网站| 欧美最新免费一区二区三区 | 在线免费观看不下载黄p国产 | 最近在线观看免费完整版| 99久久成人亚洲精品观看| 国产视频一区二区在线看| 亚洲熟妇中文字幕五十中出| aaaaa片日本免费| 久久久久免费精品人妻一区二区| 色噜噜av男人的天堂激情| 91久久精品国产一区二区成人 | 亚洲中文字幕一区二区三区有码在线看| 十八禁网站免费在线| 性色avwww在线观看| 国产伦精品一区二区三区四那| 国产极品精品免费视频能看的| 宅男免费午夜| 国产成人aa在线观看| 啦啦啦韩国在线观看视频| 91久久精品电影网| 两个人视频免费观看高清| 亚洲avbb在线观看| 中文字幕高清在线视频| eeuss影院久久| 欧美成人一区二区免费高清观看| 日韩大尺度精品在线看网址| 一区二区三区激情视频| 99精品欧美一区二区三区四区| 国产精品精品国产色婷婷| 成人18禁在线播放| 日本免费一区二区三区高清不卡| 变态另类丝袜制服| 人妻久久中文字幕网| 黄色成人免费大全| 俄罗斯特黄特色一大片| 午夜福利成人在线免费观看| 日韩人妻高清精品专区| 搡老妇女老女人老熟妇| 真实男女啪啪啪动态图| 美女大奶头视频| 最后的刺客免费高清国语| 亚洲国产精品久久男人天堂| 成年版毛片免费区| 欧美日本亚洲视频在线播放| 成年女人永久免费观看视频| 51国产日韩欧美| 国产伦一二天堂av在线观看| 亚洲熟妇中文字幕五十中出| 成人无遮挡网站| 日韩有码中文字幕| 日本在线视频免费播放| 国产在视频线在精品| 国产色婷婷99| 免费无遮挡裸体视频| 熟女电影av网| 一区福利在线观看| 女生性感内裤真人,穿戴方法视频| 国产精品三级大全| 99riav亚洲国产免费| 婷婷丁香在线五月| 91在线观看av| 男人舔奶头视频| 欧美性猛交╳xxx乱大交人| 啪啪无遮挡十八禁网站| 在线观看日韩欧美| 国产成人a区在线观看| 男女午夜视频在线观看| 欧美在线一区亚洲| 亚洲av成人精品一区久久| 色哟哟哟哟哟哟| 国产黄a三级三级三级人| 狂野欧美激情性xxxx| 欧美最新免费一区二区三区 | 97人妻精品一区二区三区麻豆| 少妇裸体淫交视频免费看高清| 日韩欧美国产在线观看| 色哟哟哟哟哟哟| 免费大片18禁| 午夜视频国产福利| 99热只有精品国产| 法律面前人人平等表现在哪些方面| 黄色成人免费大全| 一个人免费在线观看的高清视频| 日本一本二区三区精品| 免费看a级黄色片| 亚洲成人久久爱视频| 一本综合久久免费| 国产一区二区亚洲精品在线观看| 99热6这里只有精品| 婷婷精品国产亚洲av| 老汉色av国产亚洲站长工具| 欧美成人免费av一区二区三区| 我的老师免费观看完整版| 在线观看美女被高潮喷水网站 | 国产精品亚洲av一区麻豆| 九九在线视频观看精品| 变态另类丝袜制服| 国产69精品久久久久777片| 搞女人的毛片| 长腿黑丝高跟| 美女被艹到高潮喷水动态| 男女午夜视频在线观看| 免费观看的影片在线观看| 99精品在免费线老司机午夜| 99久久精品热视频| aaaaa片日本免费| 亚洲成人免费电影在线观看| 露出奶头的视频| 啦啦啦观看免费观看视频高清| 国产午夜精品久久久久久一区二区三区 | 中文字幕av成人在线电影| 国产高清有码在线观看视频| 成人一区二区视频在线观看| 欧美av亚洲av综合av国产av| 69av精品久久久久久| 亚洲男人的天堂狠狠| 亚洲中文字幕一区二区三区有码在线看| 我要搜黄色片| 宅男免费午夜| 欧美中文综合在线视频| 成人av一区二区三区在线看| 岛国在线免费视频观看| 国产伦在线观看视频一区| 黄色女人牲交| 亚洲第一欧美日韩一区二区三区| 97碰自拍视频| 国产亚洲av嫩草精品影院| 国产乱人伦免费视频| 欧美黄色片欧美黄色片| 精品99又大又爽又粗少妇毛片 | 国产成人av激情在线播放| 欧美日韩黄片免| 国产精品爽爽va在线观看网站| 色av中文字幕| ponron亚洲| 在线观看免费午夜福利视频| 国产乱人伦免费视频| 99精品欧美一区二区三区四区| 日本一二三区视频观看| 成人高潮视频无遮挡免费网站| 日本 av在线| 在线免费观看不下载黄p国产 | 午夜福利成人在线免费观看| 国产精品综合久久久久久久免费| 午夜亚洲福利在线播放| 看片在线看免费视频| 村上凉子中文字幕在线| 热99re8久久精品国产| 欧美日韩国产亚洲二区| 亚洲精品亚洲一区二区| 99热只有精品国产| 国产成人av教育| 国产精品一区二区三区四区免费观看 | av欧美777| 精品午夜福利视频在线观看一区| 国产精品久久久久久亚洲av鲁大| 18禁美女被吸乳视频| 美女高潮的动态| 欧美日韩黄片免| 精品欧美国产一区二区三| 亚洲国产精品合色在线| 一个人免费在线观看的高清视频| 成人亚洲精品av一区二区| 欧美日韩综合久久久久久 | 在线国产一区二区在线| 无遮挡黄片免费观看| 真人一进一出gif抽搐免费| 久久精品国产亚洲av涩爱 | 少妇人妻一区二区三区视频| 在线看三级毛片| 在线观看av片永久免费下载| 欧美xxxx黑人xx丫x性爽| 国产在线精品亚洲第一网站| av欧美777| 一区二区三区免费毛片| 非洲黑人性xxxx精品又粗又长| 免费在线观看日本一区| 国产伦一二天堂av在线观看| av在线蜜桃| 岛国视频午夜一区免费看| 中亚洲国语对白在线视频| 欧美成狂野欧美在线观看| 欧美一级毛片孕妇| 9191精品国产免费久久| 国产三级中文精品| 亚洲熟妇熟女久久| 欧美xxxx黑人xx丫x性爽| 两人在一起打扑克的视频| 真人做人爱边吃奶动态| 一进一出抽搐gif免费好疼| 99精品欧美一区二区三区四区| a在线观看视频网站| 最近最新中文字幕大全电影3| 精品一区二区三区人妻视频| 日本 欧美在线| 国内精品一区二区在线观看| 国产精品爽爽va在线观看网站| xxx96com| 国产国拍精品亚洲av在线观看 | 精品不卡国产一区二区三区| 18禁美女被吸乳视频| av黄色大香蕉| 国内揄拍国产精品人妻在线| 欧洲精品卡2卡3卡4卡5卡区| 欧美av亚洲av综合av国产av| 欧美极品一区二区三区四区| 精品人妻偷拍中文字幕| 欧美日韩一级在线毛片| 国产精品乱码一区二三区的特点| 最近最新中文字幕大全免费视频| 国产成人a区在线观看| 亚洲精品美女久久久久99蜜臀| 免费av毛片视频| 国产高清有码在线观看视频| 麻豆一二三区av精品| 丰满的人妻完整版| 老司机福利观看| 色噜噜av男人的天堂激情| 亚洲av免费高清在线观看| 国产老妇女一区| 国产黄a三级三级三级人| 日本撒尿小便嘘嘘汇集6| 亚洲久久久久久中文字幕| 亚洲av不卡在线观看| 国产成人a区在线观看| 久久亚洲精品不卡| 亚洲欧美激情综合另类| 757午夜福利合集在线观看| 国产精品三级大全| 日本三级黄在线观看| 午夜福利高清视频| 久久久国产成人免费| 18+在线观看网站| 丰满人妻一区二区三区视频av | 欧美激情在线99| 亚洲中文日韩欧美视频| 亚洲,欧美精品.| 人妻久久中文字幕网| 12—13女人毛片做爰片一| 免费搜索国产男女视频| 99久久成人亚洲精品观看| 一区二区三区高清视频在线| 国产高清有码在线观看视频| 国产精品亚洲av一区麻豆| 在线a可以看的网站| 国产精品久久久久久亚洲av鲁大| 黄色视频,在线免费观看| 99久久综合精品五月天人人| 在线十欧美十亚洲十日本专区| 欧美日韩黄片免| 草草在线视频免费看| 偷拍熟女少妇极品色| 午夜激情福利司机影院| 人人妻人人看人人澡| 国产不卡一卡二| 午夜精品久久久久久毛片777| 国产精品亚洲美女久久久| 欧美日韩黄片免| 午夜亚洲福利在线播放| 国产av麻豆久久久久久久| 精品电影一区二区在线| 变态另类丝袜制服| 亚洲男人的天堂狠狠| 日本成人三级电影网站| 亚洲国产精品999在线| 久久6这里有精品| 亚洲不卡免费看| 久久精品人妻少妇| 欧美zozozo另类| 精品一区二区三区av网在线观看| av在线蜜桃| 免费人成视频x8x8入口观看| 国产综合懂色| 久久婷婷人人爽人人干人人爱| 一级作爱视频免费观看| 韩国av一区二区三区四区| 国产精品香港三级国产av潘金莲| 久久久久性生活片| 亚洲成人免费电影在线观看| 久久久国产精品麻豆| 天堂影院成人在线观看| 成年女人看的毛片在线观看| АⅤ资源中文在线天堂| 精品99又大又爽又粗少妇毛片 | 欧美性猛交╳xxx乱大交人| 成熟少妇高潮喷水视频| 麻豆成人av在线观看| 嫩草影院精品99| a级一级毛片免费在线观看| 久久精品国产亚洲av香蕉五月| 男人和女人高潮做爰伦理| 国产精品一区二区免费欧美| 国产男靠女视频免费网站| 最近视频中文字幕2019在线8| 久久久久精品国产欧美久久久| 欧美日韩综合久久久久久 | 免费在线观看亚洲国产| 变态另类成人亚洲欧美熟女| 久久久国产精品麻豆| 久久久久精品国产欧美久久久| 在线观看av片永久免费下载| 午夜亚洲福利在线播放| 男女那种视频在线观看| 久久久久久人人人人人| 色综合站精品国产| 国产av一区在线观看免费| 日本免费一区二区三区高清不卡| 美女高潮喷水抽搐中文字幕| 国内少妇人妻偷人精品xxx网站| 国产视频一区二区在线看| 五月玫瑰六月丁香| 欧美一级毛片孕妇| 亚洲av成人不卡在线观看播放网| 高清日韩中文字幕在线| 国内精品久久久久久久电影| 国产激情欧美一区二区| 日韩欧美精品v在线| 欧美成人a在线观看| 夜夜躁狠狠躁天天躁| 亚洲专区中文字幕在线| 成人午夜高清在线视频| 真实男女啪啪啪动态图| 成人av一区二区三区在线看| 韩国av一区二区三区四区| 亚洲真实伦在线观看| 天美传媒精品一区二区| 国产成人a区在线观看| 亚洲精品亚洲一区二区| 最近最新中文字幕大全免费视频| 在线播放国产精品三级| 亚洲乱码一区二区免费版| 亚洲人与动物交配视频| 亚洲欧美日韩东京热| or卡值多少钱| 国产精品电影一区二区三区| 欧美av亚洲av综合av国产av| 久久久久九九精品影院| 国产熟女xx| 欧美一区二区亚洲| 午夜精品一区二区三区免费看| 亚洲成人久久性| 免费观看的影片在线观看| 少妇熟女aⅴ在线视频| 亚洲国产精品成人综合色| netflix在线观看网站| 日韩欧美一区二区三区在线观看| 桃色一区二区三区在线观看| 国产三级在线视频| av片东京热男人的天堂| 一进一出抽搐gif免费好疼| 欧美成人一区二区免费高清观看| h日本视频在线播放| 久久久精品欧美日韩精品| 人妻久久中文字幕网| 变态另类成人亚洲欧美熟女| 亚洲av第一区精品v没综合| 国产探花在线观看一区二区| 日韩 欧美 亚洲 中文字幕| 精品日产1卡2卡| 亚洲美女黄片视频| 又爽又黄无遮挡网站| 精品人妻1区二区| 在线观看免费午夜福利视频| 欧美日韩综合久久久久久 | 18禁美女被吸乳视频| 国产在视频线在精品| 久久精品人妻少妇| 久久草成人影院| 欧美又色又爽又黄视频| 18禁美女被吸乳视频| 午夜日韩欧美国产| 日韩欧美免费精品| 免费一级毛片在线播放高清视频| 国产欧美日韩一区二区三| 亚洲久久久久久中文字幕| 午夜福利高清视频| 麻豆成人午夜福利视频| 又紧又爽又黄一区二区| 90打野战视频偷拍视频| 日本在线视频免费播放| 亚洲精品在线观看二区| 色播亚洲综合网| 亚洲va日本ⅴa欧美va伊人久久| 亚洲av一区综合| 国产亚洲精品综合一区在线观看| 国产不卡一卡二| 桃色一区二区三区在线观看|