• <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
    97人妻精品一区二区三区麻豆| av天堂中文字幕网| 国内精品宾馆在线| 久久97久久精品| 肉色欧美久久久久久久蜜桃 | 99热这里只有是精品50| 欧美潮喷喷水| 狠狠精品人妻久久久久久综合| 99热这里只有是精品在线观看| 在线免费十八禁| 能在线免费观看的黄片| 成人性生交大片免费视频hd| 久久国内精品自在自线图片| 亚洲欧美清纯卡通| 春色校园在线视频观看| 简卡轻食公司| 建设人人有责人人尽责人人享有的 | 国产精品一区二区在线观看99 | 国产伦一二天堂av在线观看| 青春草视频在线免费观看| 麻豆乱淫一区二区| 欧美xxxx性猛交bbbb| 免费黄色在线免费观看| 成人av在线播放网站| 99热6这里只有精品| 久久久久性生活片| 嘟嘟电影网在线观看| 午夜福利成人在线免费观看| 成年av动漫网址| 丝瓜视频免费看黄片| 久久久a久久爽久久v久久| 男女那种视频在线观看| 午夜视频国产福利| 中文字幕人妻熟人妻熟丝袜美| 国产淫片久久久久久久久| 久久精品久久精品一区二区三区| 国产男人的电影天堂91| 久久精品综合一区二区三区| 亚洲国产精品专区欧美| 一级毛片黄色毛片免费观看视频| 亚洲av中文字字幕乱码综合| 成人鲁丝片一二三区免费| 男插女下体视频免费在线播放| 婷婷色综合大香蕉| 日日摸夜夜添夜夜添av毛片| 丰满少妇做爰视频| 九色成人免费人妻av| 亚洲伊人久久精品综合| av国产免费在线观看| 国产女主播在线喷水免费视频网站 | a级毛片免费高清观看在线播放| 国产黄片视频在线免费观看| 欧美成人a在线观看| 两个人视频免费观看高清| 日日摸夜夜添夜夜爱| 欧美成人a在线观看| 蜜桃亚洲精品一区二区三区| 九九爱精品视频在线观看| 国产亚洲av片在线观看秒播厂 | 成人毛片60女人毛片免费| 中文字幕av成人在线电影| freevideosex欧美| eeuss影院久久| 国产视频首页在线观看| 日本爱情动作片www.在线观看| 日本黄色片子视频| 少妇高潮的动态图| 日韩大片免费观看网站| 亚洲精品日本国产第一区| 亚洲在线观看片| 国产一区二区三区综合在线观看 | 秋霞在线观看毛片| 亚洲一区高清亚洲精品| 久久精品熟女亚洲av麻豆精品 | 黄色日韩在线| 肉色欧美久久久久久久蜜桃 | 日韩中字成人| 九色成人免费人妻av| 大片免费播放器 马上看| 女人被狂操c到高潮| 大片免费播放器 马上看| 亚洲真实伦在线观看| 免费观看在线日韩| 欧美精品一区二区大全| 久久久a久久爽久久v久久| 真实男女啪啪啪动态图| 九九久久精品国产亚洲av麻豆| av又黄又爽大尺度在线免费看| 男女下面进入的视频免费午夜| 美女黄网站色视频| 久久精品综合一区二区三区| 成人午夜高清在线视频| 色播亚洲综合网| 国产精品福利在线免费观看| 亚洲精品久久久久久婷婷小说| 美女黄网站色视频| 深爱激情五月婷婷| 免费黄色在线免费观看| 黄色欧美视频在线观看| 成人高潮视频无遮挡免费网站| 午夜福利网站1000一区二区三区| 亚洲综合色惰| 毛片一级片免费看久久久久| 干丝袜人妻中文字幕| 亚洲国产日韩欧美精品在线观看| 亚洲精品日韩在线中文字幕| 国产成年人精品一区二区| 97热精品久久久久久| 久久草成人影院| 亚洲无线观看免费| 男的添女的下面高潮视频| 久久久久久久久大av| 亚洲熟妇中文字幕五十中出| 综合色丁香网| 久久午夜福利片| 欧美xxxx性猛交bbbb| 蜜桃久久精品国产亚洲av| 国产欧美日韩精品一区二区| 内射极品少妇av片p| 91午夜精品亚洲一区二区三区| 免费高清在线观看视频在线观看| 国产 亚洲一区二区三区 | 国产真实伦视频高清在线观看| 欧美精品国产亚洲| 女人十人毛片免费观看3o分钟| 免费观看的影片在线观看| 久久草成人影院| 亚洲人成网站在线观看播放| 午夜福利在线观看免费完整高清在| 国产真实伦视频高清在线观看| 国国产精品蜜臀av免费| 青春草亚洲视频在线观看| 成年人午夜在线观看视频 | 在线观看人妻少妇| 国产成人精品福利久久| 国产精品 国内视频| 日韩不卡一区二区三区视频在线| 日本wwww免费看| 自拍欧美九色日韩亚洲蝌蚪91| 美女xxoo啪啪120秒动态图| 国产在视频线精品| 建设人人有责人人尽责人人享有的| 亚洲精品一区蜜桃| 久久狼人影院| 成年人免费黄色播放视频| 亚洲精品aⅴ在线观看| 日韩一区二区视频免费看| 波多野结衣av一区二区av| 亚洲视频免费观看视频| 免费播放大片免费观看视频在线观看| 亚洲四区av| 亚洲精品一二三| 亚洲色图 男人天堂 中文字幕| 在线观看免费高清a一片| 九九爱精品视频在线观看| 伦理电影大哥的女人| 妹子高潮喷水视频| 国产深夜福利视频在线观看| 熟女av电影| 人成视频在线观看免费观看| 亚洲熟女精品中文字幕| 日韩伦理黄色片| 国产日韩一区二区三区精品不卡| 亚洲精品在线美女| 亚洲,欧美精品.| 欧美亚洲 丝袜 人妻 在线| 色婷婷av一区二区三区视频| 婷婷色综合www| 国产乱人偷精品视频| 人妻一区二区av| 麻豆av在线久日| 午夜激情久久久久久久| 精品久久久精品久久久| 国产在线一区二区三区精| 亚洲国产日韩一区二区| 亚洲熟女精品中文字幕| 国产97色在线日韩免费| 国产视频首页在线观看| av电影中文网址| 一级a爱视频在线免费观看| 亚洲精品久久成人aⅴ小说| 国产成人精品久久二区二区91 | 色94色欧美一区二区| 免费在线观看黄色视频的| 午夜免费鲁丝| 丰满饥渴人妻一区二区三| 久久久欧美国产精品| 亚洲激情五月婷婷啪啪| 免费av中文字幕在线| av女优亚洲男人天堂| 久久狼人影院| 寂寞人妻少妇视频99o| 国产成人91sexporn| 嫩草影院入口| 久久人人97超碰香蕉20202| 日本黄色日本黄色录像| 五月伊人婷婷丁香| 日本爱情动作片www.在线观看| 国产精品国产三级国产专区5o| 80岁老熟妇乱子伦牲交| 日韩av不卡免费在线播放| 免费av中文字幕在线| 少妇 在线观看| 考比视频在线观看| 日韩一本色道免费dvd| 国产激情久久老熟女| av女优亚洲男人天堂| 亚洲精品久久成人aⅴ小说| 伊人亚洲综合成人网| 欧美日韩亚洲国产一区二区在线观看 | 久久国内精品自在自线图片| 国产精品久久久av美女十八| 中文字幕人妻丝袜制服| 在线观看三级黄色| 老司机亚洲免费影院| 男女无遮挡免费网站观看| 高清黄色对白视频在线免费看| 又粗又硬又长又爽又黄的视频| 亚洲一区中文字幕在线| 亚洲精品久久成人aⅴ小说| a级毛片在线看网站| 欧美精品av麻豆av| 亚洲三区欧美一区| 免费在线观看完整版高清| 两性夫妻黄色片| 观看美女的网站| 中文字幕制服av| 成人免费观看视频高清| 亚洲欧洲国产日韩| 午夜91福利影院| 亚洲国产毛片av蜜桃av| 天天躁夜夜躁狠狠久久av| 天堂8中文在线网| 美女视频免费永久观看网站| 捣出白浆h1v1| 看非洲黑人一级黄片| 精品少妇内射三级| 91成人精品电影| 亚洲欧美一区二区三区黑人 | 成年女人在线观看亚洲视频| 边亲边吃奶的免费视频| 国产片内射在线| 国产日韩欧美视频二区| 精品少妇黑人巨大在线播放| 国产极品粉嫩免费观看在线| 嫩草影院入口| 亚洲国产毛片av蜜桃av| av网站免费在线观看视频| 国产精品欧美亚洲77777| 麻豆乱淫一区二区| 日本黄色日本黄色录像| 精品国产一区二区久久| 又黄又粗又硬又大视频| 日韩视频在线欧美| 午夜日本视频在线| 天美传媒精品一区二区| 九九爱精品视频在线观看| 精品国产露脸久久av麻豆| 午夜激情久久久久久久| 少妇熟女欧美另类| 亚洲精品美女久久久久99蜜臀 | 国产探花极品一区二区| 人人妻人人澡人人看| 一本大道久久a久久精品| 午夜福利乱码中文字幕| 国产黄频视频在线观看| 免费观看性生交大片5| 欧美成人午夜免费资源| 亚洲第一区二区三区不卡| 日韩av免费高清视频| 侵犯人妻中文字幕一二三四区| 一区二区三区激情视频| 久久婷婷青草| 1024视频免费在线观看| 黄片播放在线免费| 日韩制服丝袜自拍偷拍| 欧美日韩一区二区视频在线观看视频在线| 一边亲一边摸免费视频| 人妻系列 视频| 捣出白浆h1v1| 一本—道久久a久久精品蜜桃钙片| av不卡在线播放| 青春草视频在线免费观看| 日产精品乱码卡一卡2卡三| 久久97久久精品| 国产亚洲av片在线观看秒播厂| 电影成人av| 亚洲精品久久午夜乱码| av线在线观看网站| 国产成人精品无人区| 国产一区二区 视频在线| 欧美成人午夜免费资源| 国产成人精品久久久久久| 国产精品一区二区在线不卡| 香蕉精品网在线| 国产高清不卡午夜福利| 777米奇影视久久| 亚洲五月色婷婷综合| 老汉色av国产亚洲站长工具| 日日撸夜夜添| 免费日韩欧美在线观看| 18+在线观看网站| 免费播放大片免费观看视频在线观看| 2021少妇久久久久久久久久久| 国产午夜精品一二区理论片| 日韩中字成人| 婷婷色综合www| 国产不卡av网站在线观看| 99香蕉大伊视频| 一本久久精品| av视频免费观看在线观看| 亚洲天堂av无毛| 久久国内精品自在自线图片| 亚洲精品一二三| 亚洲国产av新网站| a 毛片基地| 久久久久精品人妻al黑| 一本—道久久a久久精品蜜桃钙片| 少妇 在线观看| 久久精品人人爽人人爽视色| 亚洲国产欧美在线一区| 韩国高清视频一区二区三区| 久久久久久人人人人人| 老汉色av国产亚洲站长工具| 少妇的丰满在线观看| 777久久人妻少妇嫩草av网站| h视频一区二区三区| 99热国产这里只有精品6| 我要看黄色一级片免费的| 亚洲精品久久成人aⅴ小说| 午夜av观看不卡| 亚洲四区av| 亚洲男人天堂网一区| 各种免费的搞黄视频| 9热在线视频观看99| 亚洲国产日韩一区二区| 精品午夜福利在线看| 久热久热在线精品观看| 天堂中文最新版在线下载| 又粗又硬又长又爽又黄的视频| 超碰97精品在线观看| 国产男女超爽视频在线观看| 啦啦啦在线观看免费高清www| 老汉色∧v一级毛片| 满18在线观看网站| 高清不卡的av网站| 国产午夜精品一二区理论片| 菩萨蛮人人尽说江南好唐韦庄| 麻豆乱淫一区二区| 制服丝袜香蕉在线| 久久精品久久精品一区二区三区| av视频免费观看在线观看| 国产成人91sexporn| 天堂俺去俺来也www色官网| 日韩av在线免费看完整版不卡| 黄色视频在线播放观看不卡| 亚洲精品日韩在线中文字幕| 韩国高清视频一区二区三区| 亚洲天堂av无毛| 丝袜在线中文字幕| 日韩精品有码人妻一区| 亚洲国产精品国产精品| 18禁裸乳无遮挡动漫免费视频| av线在线观看网站| 日韩大片免费观看网站| 国产又爽黄色视频| 日韩制服骚丝袜av| 麻豆精品久久久久久蜜桃| 亚洲av中文av极速乱| 日韩免费高清中文字幕av| 欧美最新免费一区二区三区| 亚洲精品国产av成人精品| 欧美激情高清一区二区三区 | 晚上一个人看的免费电影| 婷婷色综合大香蕉| 国产在线一区二区三区精| 性少妇av在线| 国产又爽黄色视频| www.熟女人妻精品国产| 人人妻人人爽人人添夜夜欢视频| 国产av国产精品国产| 五月开心婷婷网| 亚洲成人手机| 涩涩av久久男人的天堂| 国产男人的电影天堂91| 少妇被粗大的猛进出69影院| 七月丁香在线播放| 天天影视国产精品| 熟女少妇亚洲综合色aaa.| 久久精品aⅴ一区二区三区四区 | 日本午夜av视频| a 毛片基地| 1024视频免费在线观看| 亚洲精品成人av观看孕妇| 免费高清在线观看视频在线观看| 精品国产超薄肉色丝袜足j| 男女边摸边吃奶| 热99国产精品久久久久久7| 国产男女超爽视频在线观看| 极品人妻少妇av视频| 久久综合国产亚洲精品| 黑人猛操日本美女一级片| 一本大道久久a久久精品| 丰满少妇做爰视频| 深夜精品福利| 国产一区二区三区av在线| 高清欧美精品videossex| 亚洲av在线观看美女高潮| 最新的欧美精品一区二区| 在线观看国产h片| 成年动漫av网址| 99热网站在线观看| 韩国高清视频一区二区三区| 久久99一区二区三区| 亚洲婷婷狠狠爱综合网| 亚洲国产精品999| 日本wwww免费看| 在线观看www视频免费| 久久精品国产亚洲av高清一级| 91在线精品国自产拍蜜月| 国产av一区二区精品久久| 亚洲综合色惰| 国产精品欧美亚洲77777| 狠狠精品人妻久久久久久综合| 制服诱惑二区| 免费黄色在线免费观看| 天天躁夜夜躁狠狠久久av| 亚洲国产精品成人久久小说| 国产av码专区亚洲av| 两个人看的免费小视频| av在线老鸭窝| 哪个播放器可以免费观看大片| 国产成人aa在线观看| 国产免费福利视频在线观看| 好男人视频免费观看在线| 午夜免费男女啪啪视频观看| 国产一区亚洲一区在线观看| 天天躁夜夜躁狠狠躁躁| 亚洲精品aⅴ在线观看| av免费在线看不卡| 少妇 在线观看| 欧美xxⅹ黑人| 久久99热这里只频精品6学生| 青春草视频在线免费观看| 久久久久久伊人网av| 飞空精品影院首页| 日产精品乱码卡一卡2卡三| 一区二区三区乱码不卡18| 久久亚洲国产成人精品v| 久久久国产一区二区| av线在线观看网站| 美女主播在线视频| 免费黄色在线免费观看| 国产成人精品久久久久久| 热re99久久国产66热| 成年人免费黄色播放视频| 久久综合国产亚洲精品| 亚洲精华国产精华液的使用体验| 一级毛片电影观看| 一区福利在线观看| 亚洲av福利一区| 亚洲国产精品国产精品| 69精品国产乱码久久久| 黄网站色视频无遮挡免费观看| 18在线观看网站| 国产 精品1| 午夜福利一区二区在线看| 伦理电影免费视频| 九草在线视频观看| 在现免费观看毛片| 国产极品天堂在线| 乱人伦中国视频| 大码成人一级视频| 国产成人一区二区在线| 亚洲婷婷狠狠爱综合网| 精品人妻偷拍中文字幕| 在线亚洲精品国产二区图片欧美| 精品午夜福利在线看| 熟女av电影| 99久久综合免费| 天天操日日干夜夜撸| 国产精品国产三级国产专区5o| 久久久久精品久久久久真实原创| 精品一区二区三卡| 亚洲精品久久午夜乱码| 黄频高清免费视频| 啦啦啦啦在线视频资源| 日韩一卡2卡3卡4卡2021年| 在线观看免费视频网站a站| 黑人欧美特级aaaaaa片| 免费高清在线观看日韩| 久久精品夜色国产| 精品国产一区二区久久| 人妻 亚洲 视频| 黄色毛片三级朝国网站| 天天操日日干夜夜撸| 美女视频免费永久观看网站| 日韩三级伦理在线观看| 国产精品二区激情视频| 日韩欧美精品免费久久| 午夜福利网站1000一区二区三区| 国产精品久久久久久久久免| 精品午夜福利在线看| 深夜精品福利| 99久久精品国产国产毛片| 只有这里有精品99| 91成人精品电影| 制服人妻中文乱码| 亚洲人成77777在线视频| 九色亚洲精品在线播放| 欧美bdsm另类| 亚洲精品久久成人aⅴ小说| 一区二区三区四区激情视频| 亚洲欧美一区二区三区黑人 | 男女啪啪激烈高潮av片| 熟妇人妻不卡中文字幕| 国产精品欧美亚洲77777| 国产一区二区激情短视频 | 日本午夜av视频| 欧美精品高潮呻吟av久久| 搡老乐熟女国产| 久久精品人人爽人人爽视色| 久久精品夜色国产| 亚洲伊人久久精品综合| 日韩在线高清观看一区二区三区| 色播在线永久视频| 18在线观看网站| 国产日韩欧美亚洲二区| 亚洲国产精品一区三区| 成人亚洲欧美一区二区av| 秋霞在线观看毛片| 桃花免费在线播放| 高清视频免费观看一区二区| 2021少妇久久久久久久久久久| 91aial.com中文字幕在线观看| 波多野结衣av一区二区av| 青青草视频在线视频观看| 黄频高清免费视频| 飞空精品影院首页| 日本猛色少妇xxxxx猛交久久| 黄色一级大片看看| 最近2019中文字幕mv第一页| 菩萨蛮人人尽说江南好唐韦庄| 国产成人午夜福利电影在线观看| 欧美日韩国产mv在线观看视频| freevideosex欧美| 免费黄频网站在线观看国产| 在线观看国产h片| 一级毛片黄色毛片免费观看视频| 成人二区视频| 一边亲一边摸免费视频| videosex国产| 人妻系列 视频| 中国三级夫妇交换| 不卡视频在线观看欧美| 曰老女人黄片| 日本wwww免费看| 宅男免费午夜| 99久国产av精品国产电影| av免费观看日本| 精品一品国产午夜福利视频| 看免费av毛片| 电影成人av| 97在线人人人人妻| 综合色丁香网| 欧美精品一区二区大全| 亚洲图色成人| 久久人人爽av亚洲精品天堂| 满18在线观看网站| 亚洲成人一二三区av| 国产一区二区在线观看av| 日韩电影二区| 国产成人av激情在线播放| 亚洲伊人色综图| 亚洲精品aⅴ在线观看| www日本在线高清视频| 久久久亚洲精品成人影院| 最近2019中文字幕mv第一页| 大香蕉久久成人网| 久久精品国产a三级三级三级| 又粗又硬又长又爽又黄的视频| 亚洲,欧美,日韩| 婷婷色综合www| 国产精品偷伦视频观看了| 韩国精品一区二区三区| 大片电影免费在线观看免费| 深夜精品福利| 春色校园在线视频观看| 国产精品偷伦视频观看了| 男女午夜视频在线观看| 成人影院久久| 精品国产一区二区三区久久久樱花| 黄色视频在线播放观看不卡| 精品国产乱码久久久久久小说| 青春草视频在线免费观看| 久久精品久久精品一区二区三区| 亚洲欧美精品自产自拍| 成人二区视频| 大码成人一级视频| 精品人妻熟女毛片av久久网站| 超碰成人久久| 国产 一区精品| 国产xxxxx性猛交| 久久青草综合色| 成人毛片60女人毛片免费| 国产精品久久久久久久久免| 欧美精品国产亚洲| 日韩,欧美,国产一区二区三区| 99久久精品国产国产毛片| 黄片无遮挡物在线观看| 一个人免费看片子| 国产成人av激情在线播放| 制服丝袜香蕉在线| 欧美成人精品欧美一级黄| 精品久久蜜臀av无|