基于滿足性判定的布爾網(wǎng)絡(luò)環(huán)求解算法

郭文生，楊國武，李曉瑜，高 敏

·計(jì)算機(jī)工程與應(yīng)用·

基于滿足性判定的布爾網(wǎng)絡(luò)環(huán)求解算法

郭文生1，楊國武1，李曉瑜1，高 敏2

(1. 電子科技大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院 成都 610054；2. 加州大學(xué)洛杉磯分校電子工程學(xué)院 美國 加州 洛杉磯 CA 90034)

環(huán)是布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換過程中的穩(wěn)定態(tài)，在模式檢測、基因調(diào)控網(wǎng)絡(luò)和可達(dá)性分析等領(lǐng)域都有重要的意義。計(jì)算布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換中的所有環(huán)是一個(gè)NP完全問題。該文基于全解布爾滿足性判定(SAT)算法，設(shè)計(jì)了一種求解所有小于等于指定步長環(huán)的算法。算法基于布爾網(wǎng)絡(luò)的狀態(tài)轉(zhuǎn)換函數(shù)和狀態(tài)環(huán)屬性生成合取范式形式(CNF)的問題集，通過融合沖突子句學(xué)習(xí)(CDCL)、非時(shí)序回退、阻塞子句和變量分類等技術(shù)，降低算法的計(jì)算復(fù)雜度。實(shí)驗(yàn)結(jié)果表明，該算法能夠高效地計(jì)算指定步長的環(huán)。對(duì)于無法計(jì)算所有環(huán)的復(fù)雜網(wǎng)絡(luò)，指定步長計(jì)算環(huán)的方式將更有應(yīng)用價(jià)值。

布爾網(wǎng)絡(luò); 環(huán); 滿足性判定; 阻塞子句

布爾網(wǎng)絡(luò)的穩(wěn)定狀態(tài)包括兩種：不動(dòng)點(diǎn)和環(huán)。不動(dòng)點(diǎn)是環(huán)的一種特例，即環(huán)步長為1。布爾網(wǎng)絡(luò)環(huán)的計(jì)算是一個(gè)NP完全問題[1-2]。近年來，隨著布爾滿足性判定SAT算法的不斷優(yōu)化，越來越多的布爾網(wǎng)絡(luò)問題都可以用SAT算法求解，如無邊界的符號(hào)模式檢測、可達(dá)性分析、量詞消除、基因調(diào)控網(wǎng)絡(luò)求環(huán)等[3-8]，但對(duì)于復(fù)雜布爾網(wǎng)絡(luò)的所有環(huán)的求解仍然具有非常高的計(jì)算復(fù)雜度。本文的目標(biāo)是基于SAT全解算法計(jì)算所有小于指定步長的環(huán)。

1 相關(guān)技術(shù)

1.1 基本術(shù)語

使用SAT算法求解，絕大部分應(yīng)用都需要轉(zhuǎn)換成通用的SAT問題描述形式，即CNF范式。CNF范式由所有子句的合取形式構(gòu)成，其中每個(gè)子句是若干文字(變量或非變量)的析取。每個(gè)文字是變量本身或者是變量的非。CNF范式的格式為：

式中，F(xiàn)表示要求解的滿足性問題；Ci表示子句；N表示范式中包含的子句的數(shù)量；lk表示文字，lk∈{v,?v}(v是一個(gè)變量)；k表示子句中包含文字的數(shù)量(k≤n，n為變量的數(shù)量)。

1.2 基于沖突子句學(xué)習(xí)和非時(shí)序回退的DPLL算法

Davis-Putnam-Longeman-Loveland(DPLL)算法是完全SAT求解算法的基本架構(gòu)。幾乎它是所有現(xiàn)代的完全求解算法的基礎(chǔ)，包括單文字子句消除、肯定-否定規(guī)則、原子公式消除等boolean constraint propagation(BCP)規(guī)則。而CDCL和非時(shí)序回退的技術(shù)能夠有效的降低搜索空間，進(jìn)而降低SAT算法的時(shí)間和空間復(fù)雜度[9]。

BCP算法實(shí)現(xiàn)子句單元廣播，即根據(jù)已賦值的變量推導(dǎo)未賦值的變量值。如果BCP推導(dǎo)時(shí)出現(xiàn)沖突，則調(diào)用CDCL算法進(jìn)行沖突學(xué)習(xí)并生成沖突子句。沖突子句可以避免重復(fù)的路徑搜索。CDCL算法基于蘊(yùn)含圖(implication graph)技術(shù)實(shí)現(xiàn)沖突子句的學(xué)習(xí)和非時(shí)序的決策級(jí)回退。蘊(yùn)含圖描述在搜索過程中的部分變量賦值及蘊(yùn)含關(guān)系，選擇不同的決策變量選擇和不同的BCP順序?qū)⑸刹煌奶N(yùn)含圖，因此搜索過程中蘊(yùn)含圖是動(dòng)態(tài)變化的。

1.3 基于單解求解器的全解求解算法

計(jì)算滿足性判定問題F的所有滿足解，可以基于單解求解器通過如下步驟實(shí)現(xiàn)：

1) 判斷F是否滿足。若不滿足，則輸出不滿足；否則，計(jì)算一個(gè)滿足解x1, x2,…,xn，n是問題中的變量數(shù)。

2) 用vi表示滿足解中的一個(gè)變量賦值。若解xi=0，則對(duì)應(yīng)的變量表示為?vi；否則表示為vi。因此，一個(gè)滿足解可以表示為由變量或變量的非形成的一個(gè)合取子句s。

3) 將滿足解形成的合取子句取反，即所有變量取反并形成一個(gè)析取子句c。

4) 將析取子句c加入到求解的問題集F，形成新的問題集FFc=∧。

5) 判斷新的問題集F′是否存在滿足解。若存在，則轉(zhuǎn)到步驟2)；否則輸出所有已計(jì)算的滿足解。

上述求全解的過程存在如下問題：

1) 每一次滿足解的計(jì)算都是以整個(gè)問題為基礎(chǔ)，對(duì)前一次求解過程中的搜索空間沒有記錄。

2) 沒有根據(jù)求全解的特點(diǎn)進(jìn)行搜索算法優(yōu)化。

針對(duì)上述問題，文獻(xiàn)[3]提出了阻塞子句(blocking clause)的方式。當(dāng)單解SAT求解器獲得一個(gè)滿足解時(shí)，并不停止求解過程，而是將該滿足解對(duì)應(yīng)的變量合取表示方式取反形成一個(gè)析取子句作為阻塞子句加到問題集中，繼續(xù)求解過程。通過這種方式可以保留前一次求解過程中所學(xué)習(xí)的沖突子句，并不再搜索已經(jīng)搜索過的路徑空間。然而，由于滿足性問題的滿足解可能非常多，從而導(dǎo)致阻塞子句需要較大的內(nèi)存空間，并且大量的阻塞子句也會(huì)增加問題的求解復(fù)雜度。文獻(xiàn)[4]為降低阻塞子句的數(shù)量，使用子句聚合方式對(duì)產(chǎn)生的阻塞子句集進(jìn)行蘊(yùn)含化簡，縮短阻塞子句的長度，進(jìn)而降低阻塞子句的數(shù)量。文獻(xiàn)[10]提出了基于算法避免再次獲得重復(fù)滿足解的方式，降低內(nèi)存開銷并保持求解復(fù)雜度不變。它沒有使用阻塞子句的方式避免計(jì)算重復(fù)解，而是基于決策變量與求得解的蘊(yùn)含關(guān)系生成沖突子句，進(jìn)而避免后續(xù)的計(jì)算出現(xiàn)重復(fù)的解。這種生成沖突子句的方式在本質(zhì)上等同于生成阻塞子句的方式。同時(shí)，它提出了求解問題中變量劃分的方法，它將要求解問題中的變量劃分成兩類：重要變量集和不重要變量集。在搜索過程中先選擇重要變量進(jìn)行決策賦值，當(dāng)重要變量全部賦值完成后才對(duì)不重要變量進(jìn)行決策賦值。然而該算法是基于CNF范式的求解，其重要變量和非重要變量沒有結(jié)合具體問題進(jìn)行定義。文獻(xiàn)[11]為降低阻塞子句的數(shù)量并降低后續(xù)計(jì)算的搜索空間使用最短阻塞子句的方式計(jì)算全解，它基于覆蓋算法最小化滿足片段減少阻塞子句中的文字?jǐn)?shù)，但該算法使用的覆蓋算法本身復(fù)雜度也比較高，對(duì)于問題子句數(shù)和變量數(shù)多的求解問題計(jì)算復(fù)雜度較大。

上述求全解算法只考慮了如何避免已求得的滿足解的問題，而計(jì)算不動(dòng)點(diǎn)、基因調(diào)控網(wǎng)絡(luò)吸引區(qū)求解等問題在計(jì)算過程中不能僅避免已求得的滿足解，還需要避免已經(jīng)計(jì)算的不動(dòng)點(diǎn)或狀態(tài)環(huán)。

2 布爾網(wǎng)絡(luò)環(huán)求解算法

2.1 基于狀態(tài)轉(zhuǎn)換函數(shù)和環(huán)屬性創(chuàng)建求解問題

布爾網(wǎng)絡(luò)描述的是變量之間的相互依賴關(guān)系，每個(gè)變量的值只能是0或1。變量的下一個(gè)時(shí)刻的值由依賴節(jié)點(diǎn)的當(dāng)前時(shí)刻的值確定，即：

式中，vi′表示節(jié)點(diǎn)i的下一個(gè)時(shí)刻的狀態(tài)值；v1，v2,…,vm表示節(jié)點(diǎn)i依賴的m個(gè)節(jié)點(diǎn)的當(dāng)前時(shí)刻的值。

布爾網(wǎng)絡(luò)的環(huán)是布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換過程中的穩(wěn)定狀態(tài)。如果環(huán)的步長為N，則布爾網(wǎng)絡(luò)至少需要經(jīng)過N個(gè)時(shí)刻的狀態(tài)遷移才能進(jìn)入環(huán)狀態(tài)。因此，根據(jù)布爾網(wǎng)絡(luò)的狀態(tài)轉(zhuǎn)換函數(shù)，可以通過N步展開的方式生成包含N+1個(gè)布爾網(wǎng)絡(luò)狀態(tài)的轉(zhuǎn)換路徑，即：

式中，path表示布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換圖中的一條路徑；s0表示網(wǎng)絡(luò)的初始狀態(tài)；sk=vk1,vk2,…,vkn表示第k時(shí)刻網(wǎng)絡(luò)的狀態(tài)。

同時(shí)，步長小于等于N的所有環(huán)的屬性p可以描述成為：

根據(jù)式(2)～式(4)可以得到計(jì)算步長小于等于N的環(huán)的求解問題集，并可以通過引入輔助變量的方式將其轉(zhuǎn)換成CNF形式。

2.2 基于SAT全解算法的環(huán)計(jì)算

基于阻塞子句、沖突蘊(yùn)含圖生成阻塞子句和變量分類等SAT全解算法的實(shí)現(xiàn)技術(shù)，結(jié)合布爾網(wǎng)絡(luò)轉(zhuǎn)換關(guān)系和環(huán)屬性描述方式，本文提出了求解步長小于等于N的環(huán)的求解算法。其算法的基本流程為：Input: CNF范式F，變量集V，環(huán)步長N；

Output：全部滿足解all-solution或不滿足UNSAT；初始化:

L=NULL; //L是確定賦值的文字集合；

DecisionLevel = 0; //DecisionLevel是搜索的深度；Status = SAT;

生成CNF問題集F： cisionVars(F);

IF (BCP(F,L)==CONFLICT) THEN Return UNSAT；WHILE (Status == SAT)

Begin

preClauseCount =sizeof()F; //獲得原始問題的子句數(shù)量；

WHILE (sizeof(L) ＜ sizeof(V)) //sizeof()獲得變量的數(shù)量；

Begin

l=PickBranchLit(F,VVar(L)); //從未賦值的變量中選擇一個(gè)變量賦值，Var(L)是已賦值的變量集合；

Add(l, L); DecisionLevel++; //增加賦值變量到解集L；

IF (BCP(F, L) == CONFLICT)

Begin

DecisionLevel = CDCL(F, L);

If (DecisionLevel ＜ curDecisionLevel)

Begin

removeClausesFrom(preClauseCount);

c=GenBlockClause(D);

FFc=∧;

End

IF (DecisionLevel==0) Status = UNSAT, Break;

ELSE BackJump(DecisionLevel);

End

End

curDecisionLevel = DecisionLevel;

s =L;//獲得一個(gè)滿足解；

c=GenBlockClause(D);

FFc=∧;

BackJump(DecisionLevel ? 1);

End

IF (Sizeof(All-Solution) ＞ 0) Return All-Solution;

ELSE Return UNSAT;

PickBranchLit( )函數(shù)實(shí)現(xiàn)決策變量的選擇并為其賦值。根據(jù)轉(zhuǎn)換CNF過程中存在大量輔助變量的特性，選擇決策變量時(shí)采用了變量分類的方式減少?zèng)Q策變量的選擇空間。setDecisionVars( )函數(shù)用于設(shè)置變量的屬性，即該變量是否可以作為決策變量。GenBlockClause( )函數(shù)根據(jù)當(dāng)前的決策變量賦值獲得阻塞子句。參數(shù)D表示決策級(jí)為k時(shí)的所有決策變量賦值對(duì)應(yīng)的文字集合D={d1, d2,…,dk}，則GenBlockClause( )函數(shù)生成的阻塞子句為c= ?d1∨?d2∨…∨?dk。

2.3 基于變量分類的決策文字選擇優(yōu)化

為提高搜索速度并降低搜索空間，本文將待選擇變量分為兩類：決策變量和蘊(yùn)含變量。決策變量是布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換過程中對(duì)應(yīng)的狀態(tài)變量，蘊(yùn)含變量是布爾網(wǎng)絡(luò)轉(zhuǎn)換成CNF范式過程中引入的輔助變量。本文中布爾網(wǎng)絡(luò)的描述形式采用的是類似于berkeley logic interchange format (BLIF)的格式，轉(zhuǎn)換關(guān)系示例如表1所示。

表1 布爾網(wǎng)絡(luò)轉(zhuǎn)換關(guān)系描述示例

表1能夠準(zhǔn)確的描述布爾網(wǎng)絡(luò)節(jié)點(diǎn)之間的依賴關(guān)系，并根據(jù)該依賴關(guān)系得到對(duì)應(yīng)的布爾網(wǎng)絡(luò)狀態(tài)轉(zhuǎn)換函數(shù)。在同步布爾網(wǎng)絡(luò)中，給定一個(gè)布爾網(wǎng)絡(luò)的轉(zhuǎn)換步數(shù)N后，可以根據(jù)轉(zhuǎn)換關(guān)系展開得到布爾網(wǎng)絡(luò)的狀態(tài)轉(zhuǎn)換圖，并將其轉(zhuǎn)換成CNF形式。然而在轉(zhuǎn)換過程中將會(huì)引入大量的輔助變量。表1中的每一個(gè)轉(zhuǎn)換定義項(xiàng)都需要引入一個(gè)輔助變量。下面以表1中節(jié)點(diǎn)2的下一個(gè)狀態(tài)轉(zhuǎn)換函數(shù)為例描述轉(zhuǎn)換過程：

1)若節(jié)點(diǎn)的當(dāng)前狀態(tài)為1，則表示為vi( i∈{1,2,3})，否則表示為?vi。

3) 根據(jù)表1中(.n 2 2 1 3)的描述，其轉(zhuǎn)換函數(shù)v2′=f( v1, v3)，同時(shí)其后的兩行分別表示v2′=?v1∧v3=1和v2′=v1∧?v3=1，即節(jié)點(diǎn)2的轉(zhuǎn)換關(guān)系函數(shù)可表示為：

4) 針對(duì)轉(zhuǎn)換關(guān)系函數(shù)中的每一個(gè)合取項(xiàng)引入一個(gè)輔助變量y1, y2，并令y1=?v1∧v3,y2=v1∧?v3，則節(jié)點(diǎn)2的轉(zhuǎn)換關(guān)系函數(shù)可表示為：

5)步驟4)的轉(zhuǎn)換關(guān)系轉(zhuǎn)換成CNF范式的子句集為：

根據(jù)上述轉(zhuǎn)換過程可以看出，輔助變量的賦值是由節(jié)點(diǎn)狀態(tài)值所蘊(yùn)含的，因此在SAT求解過程中只要確定了節(jié)點(diǎn)狀態(tài)值，則輔助變量的賦值能夠根據(jù)蘊(yùn)含關(guān)系確定，因此在PickBranchLit( )函數(shù)選擇決策變量的過程中不需要選擇輔助變量作為決策變量，進(jìn)而降低SAT求解的搜索空間。

2.4 基于蘊(yùn)含圖的決策變量生成阻塞子句優(yōu)化

根據(jù)計(jì)算全解和增加子句的過程，可將要求解的問題分成兩部分：原始的問題F和阻塞子句集B。SAT問題F的一個(gè)滿足解si( x1, x2,…,xn)可以用合取子句ci=l1∧l2∧…∧ln表示，如果xi=1，則子句中對(duì)應(yīng)的文字li=vi；否則li=?vi。因此，所有已獲得的m個(gè)滿足解的集合將形成一個(gè)析取disjunctive normal form(DNF)范式，其格式為：

基于滿足解集，可以得到阻塞子句集BS=?。在計(jì)算是否存在1m+個(gè)滿足解時(shí)，需要將B加入到問題集F中，即FFB=∧，以避免獲得重復(fù)的解。顯然，S中包含的子句越多且每個(gè)子句中的文字?jǐn)?shù)越多，則計(jì)算1m+個(gè)滿足解的時(shí)間和空間復(fù)雜度越大。

優(yōu)化的目標(biāo)之一是降低阻塞子句中文字的數(shù)量。沖突子句學(xué)習(xí)的SAT求解算法會(huì)在求解過程中基于選擇的決策變量進(jìn)行蘊(yùn)含推理，進(jìn)而生成局部蘊(yùn)含圖。蘊(yùn)含圖示例如圖1所示。

圖1中待求解的CNF范式由4個(gè)子句構(gòu)成F=C1∧C2∧C3∧C4。xi=a@l表示決策級(jí)為l時(shí)xi的值為a。子句數(shù)據(jù)庫為C1=x1∨x2，C2=?x2∨?x3，C3=x3∨x4∨x5，C4=?x5∨x6。決策級(jí)為1時(shí)，決策變量及分配的值為{x1=0@1}，蘊(yùn)含分配的值為{x2=1@1, x3=0@1}。決策級(jí)為2，決策變量及分配的值為{x4=0@2}，蘊(yùn)含分配的值為{x5=1, x6=1}。最后獲得可滿足解{x1=0, x2=1,x3=0, x4=0, x5=1, x6=1}。

圖1 SAT求解過程中的蘊(yùn)含圖示例

根據(jù)圖1可以看到，當(dāng)前的可滿足解s={?v1, v2,?v3,?v4, v5, v6}是由兩個(gè)決策變量的賦值d={x1=0@1,x4=0@2}確定的。因此，為避免下一次計(jì)算出現(xiàn)重復(fù)的解，則生成的阻塞子句是?v1∧?v4的非，即v1∨v4。顯然，使用決策變量生成阻塞子句的方式極大的降低了阻塞子句中文字的數(shù)量。

優(yōu)化目標(biāo)之二是減少阻塞子句的數(shù)量。在基于沖突子句的SAT求解過程中，當(dāng)獲得一個(gè)滿足解時(shí)，采用時(shí)序回退的算法計(jì)算下一個(gè)滿足解。即全解搜索方式采用深度優(yōu)先搜索算法。在深度優(yōu)先搜索時(shí)，如果沖突回退的決策級(jí)比當(dāng)前的決策級(jí)小，則表明當(dāng)前決策級(jí)之下已經(jīng)不存在滿足解，則可以刪除當(dāng)前產(chǎn)生的所有阻塞子句，并基于回退的決策級(jí)backlevel生成一個(gè)阻塞子句c=?d1∨?d2∨…∨?dbacklevel，表示backlevel之后的所有滿足解都已經(jīng)被計(jì)算，并使用一個(gè)阻塞子句c避免所有搜索過的滿足解空間。

3 實(shí)驗(yàn)結(jié)果分析

基于Minisat求解器[12]實(shí)現(xiàn)了不動(dòng)點(diǎn)和步長小于等于K的周期性環(huán)的SAT全解算法period cycles algorithm based on decision node and important variable(PC-DI)。并選擇了一個(gè)基于SAT計(jì)算所有環(huán)的求解器BNS[5]作為比較工具。實(shí)驗(yàn)使用與文獻(xiàn)[5]的測試案例和N-K隨機(jī)布爾網(wǎng)絡(luò)作為測試基準(zhǔn)。N-K網(wǎng)絡(luò)使用R環(huán)境中的BoolNet包隨機(jī)生成8個(gè)最大環(huán)長不超過100的布爾網(wǎng)絡(luò)。測試平臺(tái)的配置為Intel Xeon CPU@3.3 GHz 8-Core(測試時(shí)只用了一個(gè)核)，內(nèi)存為128 GB，操作系統(tǒng)是Ubuntu 12.04。

實(shí)驗(yàn)分析了兩方面的性能：所有周期性環(huán)求解性能和指定步長周期性環(huán)求解性能。

為了使用本文的算法計(jì)算所有的周期環(huán)，首先使用BNS計(jì)算出所有環(huán)并獲得最大的環(huán)長，然后以最大環(huán)長為指定步長運(yùn)行本文的求解器，測試結(jié)果如表2所示。

表2 所有環(huán)求解計(jì)算結(jié)果

圖2 指定步長環(huán)的運(yùn)行時(shí)結(jié)果

實(shí)驗(yàn)結(jié)果顯示本文算法在計(jì)算環(huán)的最大步長小于100的真實(shí)案例和隨機(jī)案例中都具有較大的性能優(yōu)勢。

基于表2的測試結(jié)果，選擇其中4個(gè)BNS計(jì)算時(shí)間在100 s以上的案例(Random2, Random4, Random6, Random8)進(jìn)行指定步長環(huán)計(jì)算的分析。對(duì)每一個(gè)測試案例指定不同的步長進(jìn)行測試。指定的步長初始值為1，每次增加4個(gè)步長，最大指定步長設(shè)置為69(大于所有測試案例的環(huán)的最大步長)。測試結(jié)果如圖2和圖3所示。

圖2比較的是指定最大環(huán)步長時(shí)計(jì)算所有周期環(huán)的時(shí)間，圖3比較的是指定最大環(huán)步長時(shí)計(jì)算出的周期環(huán)的數(shù)量。Random2、Random4、Random6和Random8的所有周期環(huán)分別是5 632個(gè)、24個(gè)、2 280個(gè)和478個(gè)。圖2顯示Random4和Random8的運(yùn)行時(shí)間增加比較平緩，Random2和Random6分別在指定步長為61和69時(shí)運(yùn)行時(shí)間增加較大。結(jié)合圖3可以看出，Random2和Random6分別在指定步長為61和69時(shí)周期性環(huán)數(shù)顯著增加。

圖3 小于等于指定步長環(huán)的總環(huán)數(shù)

實(shí)驗(yàn)結(jié)果顯示，本文算法對(duì)于環(huán)長分布比較均勻的布爾網(wǎng)絡(luò)具有較低的計(jì)算復(fù)雜度，并且指定的步長與運(yùn)行時(shí)間成線性增加的關(guān)系。同時(shí)，對(duì)于運(yùn)行時(shí)間較長且環(huán)長分布不均勻的案例(步長大的環(huán)占所有環(huán)的比例較高)，其主要的時(shí)間開銷集中在步長大的周期環(huán)計(jì)算過程中。

基于實(shí)驗(yàn)結(jié)果可以看到，當(dāng)指定的步長小于最大狀態(tài)環(huán)步長時(shí)，算法計(jì)算復(fù)雜度較低。因此本文算法可以通過指定步長的方式求解更復(fù)雜的布爾網(wǎng)絡(luò)的狀態(tài)環(huán)。對(duì)于無法在有限的時(shí)間內(nèi)計(jì)算所有周期環(huán)的案例，本文將具有更大的優(yōu)勢。

4 結(jié) 束 語

本文提出了一種高效的周期性狀態(tài)環(huán)求解算法。為降低決策變量的選擇空間提升搜索速度，該算法將布爾網(wǎng)絡(luò)轉(zhuǎn)換成CNF過程中引入的輔助變量標(biāo)記為非決策變量。通過引入基于蘊(yùn)含圖技術(shù)建立阻塞子句的方式，該算法能夠降低阻塞子句的數(shù)量并實(shí)現(xiàn)非時(shí)序題集的方式，可以充分利用SAT全解求解算法計(jì)算狀態(tài)環(huán)。實(shí)驗(yàn)結(jié)果表明，該算法具有較低的計(jì)算復(fù)雜度，并且能夠?qū)?fù)雜的網(wǎng)絡(luò)進(jìn)行指定步長的狀態(tài)環(huán)求解。

[1] ZHAO Q. A remark on "scalar equations for synchronous boolean networks with biological applications" by C. Farrow, J. Heidel, J. Maloney, and J. Rogers[J]. IEEE Transactions on Neural Networks, 2005, 16(6): 1715-1716.

[2] T AKUTSU, S KOSUB, A A MELKMAN, et al. Finding a periodic attractor of a Boolean network[J]. Transactions on Computational Biology and Bioinformatics, 2012, 9(5): 1410-1421.

[3] MCMILLAN K L. Applying SAT methods in unbounded symbolic model checking[C]//14th International Conference on Computer Aided Verification. Denmark: Springer, 2002.

[4] CHAUHAN P, CLARKE E M, KROENING D. Using SAT based image computation for reachability analysis[M]. The Netherlands: Springer, 2003.

[5] DUBROVA E, TESLENKO M. A SAT-based algorithm for finding attractors in synchronous Boolean networks[J]. Transactions on Computational Biology and Bioinformatics (TCBB), 2011, 8(5): 1393-1399.

[6] ZHENG De-sheng, YANG Guo-wu, LI Xiao-yu, et al. An efficient algorithm for computing attractors of synchronous and asynchronous Boolean networks[EB/OL]. [2014-01-01] http://journals.plos.org/plosone/article?id=10.1371/journal.p one.0060593.

[7] GUO W, YANG G, WU W, et al. A parallel attractor finding algorithm based on Boolean satisfiability for genetic regulatory networks[EB/OL]. [2014-01-03] http://journals. plos.org/plosone/article?id=10.1371/journal.pone.0094258.

[8] BRAUER J, KING A, KRIENER J. Existential quantification as incremental SAT[C]//23rd International Conference on Computer Aided Verification. Snowbird UT , USA: Springer, 2011.

[9] LIMA J F. Boolean satisfiability solvers: Techniques, implementations and analysis[J]. Electrónica e Telecomunica??es S. A., 2013, 5(2): 218-225.

[10] GRUMBERG O, SCHUSTER A, YADGAR A. Memory efficient all-solutions SAT solver and its application for reachability analysis[C]//5th international confrence on Formal Methods in Computer-Aided Design. Texas, USA: Springer, 2004.

[11] YU Y, SUBRAMANYAN P, TSISKARIDZE N, MALIK S. All-SAT using minimal blocking clauses[C]//27th International Conference on VLSI Design and 13th International Conference on Embedded Systems. Mumbai, India: IEEE, 2014.

[12] EEN N, SORENSSON N. Minisat 2.2.0[CP/DK]. [2014-02-02]. http://minisat.se/downloads/minisat-2.2.0.tar.gz.

編 輯 葉 芳

SAT-Based Algorithm for Finding Cycles in a Boolean Network

GUO Wen-sheng1, YANG Guo-wu1, LI Xiao-yu1, and GAO Min2

(1. School of Computer Science and Technology, University of Electronic Science and Technology of China Chengdu 610054; 2. School of Electronic Engineering, University of California-Los Angeles Los Angeles Califonia USA 90034)

A cycle which is a steady state in Boolean network state transition is important in modeling checking, genetic regulatory networks and reachability analysis. Obtaining all the cycles in Boolean network state transition is a NP complete problem. In this paper, we proposes an algorithm for solving all the cycles which have less than or equal to the assigned step length based on all-solution Boolean satisfiability (SAT) algorithm. By extending the state transition function of a Boolean network and the property of cycles, this algorithm creates a problem set in conjunctive normal form (CNF) and incorporates techniques such as conflict-driven clause learning (CDCL), non-chronological backtracking, blocking clause and variable classification to decrease computational complexity. Experiment result shows that this algorithm is efficient for solving the cycles. For large scale complex network that is hard to get all the cycles, this algorithm delivers more practical value.

blocking clause; boolean networks; boolean satisfiability; cycles

TP301.6

A

10.3969/j.issn.1001-0548.2015.06.015

2014 ? 05 ? 09；

2014 ? 09 ? 12

國家自然科學(xué)基金(61272175)

郭文生(1976 ? )，男，博士生，副教授，主要從事形式化方法和軟件測試技術(shù)方面的研究.