唐 傲,王曉峰,2,何 飛

(1.北方民族大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)院,寧夏 銀川 750021; 2.北方民族大學(xué)圖像圖形智能處理國(guó)家民委重點(diǎn)實(shí)驗(yàn)室,寧夏 銀川 750021)

1 引言

在計(jì)算機(jī)科學(xué)和數(shù)理邏輯中,SAT(SATisfiability)問(wèn)題是指判定命題邏輯公式的可滿足性問(wèn)題。20世紀(jì)70年代初,SAT問(wèn)題被多倫多大學(xué)的Cook[1]證明是非確定性多項(xiàng)式完全NPC(Non- deterministic Polynomial Complete)問(wèn)題,也是首個(gè)被證明了的NPC問(wèn)題[2]。SAT問(wèn)題屬于NP問(wèn)題,且是NP難問(wèn)題。許多問(wèn)題如等價(jià)性檢查、自動(dòng)測(cè)試生成和自動(dòng)定理證明等都可以在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)化為SAT問(wèn)題進(jìn)行求解。SAT求解器是一種廣泛應(yīng)用于多個(gè)實(shí)際應(yīng)用領(lǐng)域的核心技術(shù),如限界模型檢測(cè)[3]、軟硬件形式化驗(yàn)證[4]、人工智能[5]和RTL(Register Transfer Level)驗(yàn)證[6]等。在經(jīng)典領(lǐng)域中,SAT求解器發(fā)揮著重要的作用。命題邏輯并不是邏輯學(xué)的基礎(chǔ),亞里士多德的三段論邏輯[7]更接近于一階謂詞邏輯而不是命題邏輯。隨著問(wèn)題的研究和發(fā)展,人們已經(jīng)認(rèn)識(shí)到基于命題邏輯的SAT在描述能力和抽象層次上存在顯著的局限性。因此,人們需要一種比SAT更好的表達(dá)方式,以獲得更高的描述能力和抽象層次。當(dāng)前,可滿足性問(wèn)題的研究已經(jīng)轉(zhuǎn)向了更高的抽象層次,更接近于高層次設(shè)計(jì)應(yīng)用的趨勢(shì)。在這種趨勢(shì)下,SAT問(wèn)題被擴(kuò)展為可滿足性模理論SMT(Satisfiability Modulo Theories)問(wèn)題,基于一階邏輯的SMT得到了廣泛的關(guān)注。近年來(lái),隨著融合沖突學(xué)習(xí)機(jī)制的DPLL(Davis Putnam Logemann Loveland)算法的出現(xiàn),SAT問(wèn)題的研究取得了顯著進(jìn)展。研究人員已經(jīng)提出了眾多求解可滿足性問(wèn)題的算法,且其擴(kuò)展問(wèn)題也相繼得到關(guān)注和研究,如最大可滿足問(wèn)題(Max-SAT)[8,9]、SAT計(jì)數(shù)問(wèn)題(#SAT)[10,11]和SMT計(jì)數(shù)問(wèn)題(#SMT)[12]。

經(jīng)過(guò)擴(kuò)展,SMT面向一階邏輯進(jìn)行建模,在SAT的基礎(chǔ)上補(bǔ)充了量詞和項(xiàng),其背景理論中的原子公式不僅可以是命題,也可以是謂詞。因此,SMT的描述能力更強(qiáng)、抽象層次更高,更接近于字級(jí)建模,具有更加廣闊的應(yīng)用前景。SMT支持的典型背景理論包括整數(shù)、實(shí)數(shù)、未解釋函數(shù)、數(shù)組和位向量等理論。SMT求解的具體實(shí)現(xiàn)被稱為SMT求解器(SMT solver)。SMT求解器起源于20世紀(jì)70年代末80年代初,當(dāng)時(shí)一些研究人員為形式化設(shè)計(jì)了判定算法。直到20世紀(jì)90年代,研究人員對(duì)大規(guī)模問(wèn)題的SMT求解器進(jìn)行研究。在過(guò)去的20年,SAT求解技術(shù)的巨大進(jìn)步以及命題可滿足性和可滿足性模理論在許多工業(yè)中的廣泛應(yīng)用,說(shuō)明SMT近年來(lái)已經(jīng)發(fā)展成為一個(gè)非?；钴S的研究領(lǐng)域。由于SMT研究的發(fā)展和技術(shù)的進(jìn)步,現(xiàn)在有許多強(qiáng)大成熟的SMT求解器,例如MathSAT5[13]、CVC5[14]、Boolector[15]、Yices2[16]、Z3[17]、SMTInterpol[18]、openSMT2[19]和SMT-RAT[20],正在快速擴(kuò)展的應(yīng)用程序集中使用。目前,SMT求解器應(yīng)用在處理器驗(yàn)證[21]、等價(jià)性檢查[22]、有界和無(wú)界模型檢測(cè)[23]、謂詞抽象[24]、RTL級(jí)設(shè)計(jì)驗(yàn)證[25]、自動(dòng)測(cè)試用例生成[26]、類型檢查[27]、規(guī)劃、調(diào)度和優(yōu)化等領(lǐng)域。

2 基本概念和定義

SMT問(wèn)題是判定帶有背景理論的一階邏輯公式的可滿足性問(wèn)題。這些理論包括數(shù)學(xué)理論和計(jì)算機(jī)領(lǐng)域中的數(shù)據(jù)結(jié)構(gòu)理論等。一階邏輯是一種比命題邏輯更強(qiáng)大的邏輯體系,它擴(kuò)展了命題邏輯,并引入了可量化的變量。一階邏輯公式由非邏輯符號(hào)和邏輯連接符組成,其中非邏輯符號(hào)包括命題變?cè)统Ｔ€(gè)體變?cè)统Ｔ?、謂詞變?cè)统Ｔ约昂瘮?shù)變?cè)统Ｔ?。一個(gè)一階邏輯,如果它包括一系列可量化的變?cè)?、一個(gè)或多個(gè)有意義的謂詞符號(hào),由一組包含有意義的謂詞符號(hào)的公理所組成,針對(duì)特定的論域進(jìn)行建模,那么它就是一個(gè)一階理論。這些特性使得一階邏輯非常適合用于描述復(fù)雜的邏輯問(wèn)題。

2.1 命題邏輯

例1給定一個(gè)命題公式:

φ=p1∧(p1∨p3)∧(p2∨p3)

命題變?cè)猵或者命題變?cè)姆穸╬稱為文字L(Literal)。若干個(gè)文字的析取構(gòu)成一個(gè)子句[28],記為C=L1∨L2∨L3∨…∨Ln。若干個(gè)子句的合取構(gòu)成一個(gè)合取范式CNF(Conjunctive Normal Form)公式,記為F=C1∧C2∧…∧Cm。如例1給定的命題公式φ是一個(gè)CNF公式,其中子句C1:(p1),C2:(p1∨p3)和C3:(p2∨p3)。研究SAT問(wèn)題是否具有可滿足性,即判斷是否存在一組指派能夠使CNF公式為真。

2.2 一階邏輯

定義1設(shè)一個(gè)無(wú)限集S是類型的集合,多類型簽名(Many-sorted Signature)Σ是一個(gè)包含ΣS∈S類型集合、函數(shù)符號(hào)集合ΣF、謂詞符號(hào)集合ΣP和變量集合ΣX的四元組,記為Σ=(ΣS,ΣF,ΣP,ΣX),滿足以下條件:

(1)δ1,δ2,…,δn;δi∈ΣS,1≤i≤n。

(2)f∈ΣF是一個(gè)形式為δ1×δ2×…×δn→δ的n元函數(shù),當(dāng)n=0時(shí),f是一個(gè)常量符號(hào)。

(3)p∈ΣP是一個(gè)形式為δ1×δ2×…×δn→δ的n元謂詞,當(dāng)n=0時(shí),p是一個(gè)命題符號(hào)。

(4)在變量集合ΣX中,每個(gè)變量與S中的一個(gè)類型δi對(duì)應(yīng)。

定義2項(xiàng)集(term)歸納定義如下:

(1)若x∈ΣX是具有類型δ的變量,且x為個(gè)體變?cè)騻€(gè)體常元,則x∈term;

(2)若f(t1,t2,…,tn)∈ΣF,n≥0,是具有類型δ的函數(shù),f為n元函數(shù)變?cè)虺Ｔ?其中ti(1≤i≤n,n∈N+)為項(xiàng),則f(t1,t2,…,tn)∈term。當(dāng)n=0時(shí),f稱為個(gè)體變?cè)騻€(gè)體常元;

(3)任意項(xiàng)集都能夠通過(guò)有限次應(yīng)用上述規(guī)則(1)和規(guī)則(2)得到。

定義3原子公式定義如下:

若p(t1,t2,…,tn)∈ΣP是n元謂詞,n≥0,p為n元謂詞變?cè)虺Ｔ?其中ti(1≤i≤n,n∈N+)為項(xiàng),則p(t1,t2,…,tn)稱為原子公式。當(dāng)n=0時(shí),p稱為命題變?cè)蛎}常元。

定義4合式公式(formula)歸納定義[29]如下:

(1)若p∈ΣP,則p∈formula;

(2)若p∈formula,則p∈formula;

(3)若φ0∈formula且φ1∈formula,則φ0⊙φ1∈formula,其中⊙∈{∧,∨,→,?};

(4)若φ0∈formula,則?x:δ.φ0∈formula與?x:δ.φ0∈formula;

(5)任意formula都能夠通過(guò)有限次應(yīng)用規(guī)則(1)～規(guī)則(4)得到。

因此,一階邏輯公式φ表示[29]為:

φ:=p(t1,t2,…,tn)|t1=t2|φ0|

φ0∧φ1|φ0∨φ1|(?x:δ.φ0)|(?x:δ.φ1)

(1)

其中,ti(1≤i≤n,n∈N+)為項(xiàng),p為n元謂詞變?cè)?/p>

定義5模型是一個(gè)二元組M=(|M|δ,Σ),|M|δ為簽名Σ所有類型的非空解釋域。

公式φ中一個(gè)項(xiàng)t的賦值為M[x]=M(x),M[f(t1,t2,…,tn)]=M(f)(M[t1],M[t2],…,M[tn])。若μ∈|M|δ,模型M將具有δ類型的變量x賦值為μ,記為M{x→μ}。

…,M(tn))∈M(p);

定義7理論(Theory):

3 常見(jiàn)背景理論

在SMT中,人們感興趣的模型不是任意的模型,而是在給定理論T下滿足對(duì)某個(gè)簽名中符號(hào)解釋的模型。這些模型受到T的約束,能夠保證其符號(hào)解釋的一致性和可靠性。下面簡(jiǎn)單介紹一些常見(jiàn)的背景理論。

3.1 線性算數(shù)

線性算數(shù)LA(Linear Arithmetic)理論是只有“+”“-”的算數(shù)函數(shù)理論,按數(shù)據(jù)類型可分為線性實(shí)數(shù)運(yùn)算和線性整數(shù)運(yùn)算,它們都是通過(guò)任意未解釋常量擴(kuò)展的。其定義形式如下所示:

在線性實(shí)數(shù)LRA(Linear Real Arithmetic)理論中,x1,x2,…,xi是實(shí)數(shù)變量,在線性整數(shù)理論LIA(Linear Integer Arithmetic)中,x1,x2,…,xi是整數(shù)變量。在上面的定義中,可以使用“=”“≤”表示其他的不等式,如下所示:

(1)Σiaixi>k改寫(xiě)為(Σiaixi≤k);

(2)Σiaixi≥k改寫(xiě)為Σi(-aixi)≤(-k);

(3)Σiaixi

(4)Σiaixi≠k改寫(xiě)為Σiaixi≤(k-1)∨(Σiaixi≤k)。

上面的(3)和(4)僅在LIA中有效。對(duì)于LRA略有變化,即將Σiaixi

需要注意的是,在算數(shù)理論中引入乘法會(huì)大大增加問(wèn)題的復(fù)雜性,因此在實(shí)踐中通常會(huì)避免使用。基本公式的合取范式在整數(shù)情況下會(huì)變得無(wú)法判定。雖然在實(shí)際情況下是可判定的,但其復(fù)雜度會(huì)達(dá)到雙指數(shù)級(jí)別。然而,在建模和推理系統(tǒng)時(shí),算數(shù)理論非常有用,尤其是在建模有限集合、程序算數(shù)、指針和內(nèi)存操作等方面。因此,盡管存在一些復(fù)雜性問(wèn)題,仍然需要在實(shí)踐中使用算數(shù)理論去解決特定問(wèn)題。如例2所示是一個(gè)典型的LA公式φ:

例2φ=(x1+2x2≤2)∧((3x3+4x4+5x5=2)∨(-x2-x3≤3))

3.2 差分邏輯

差分邏輯DL(Difference Logic)理論是線性算數(shù)理論的特殊情況,其定義形式如下所示:

在實(shí)數(shù)差分邏輯RDL(Real Difference Logic)中,x1,x2,…,xi是實(shí)數(shù)變量;在整數(shù)差分邏輯IDL(Integer Difference Logic)中,x1,x2,…,xi是整數(shù)變量。以差分邏輯為背景理論的一階邏輯公式求解時(shí),通過(guò)使用加權(quán)有向圖(Weighted Directed Graph)[31],可以將一階邏輯公式轉(zhuǎn)化為圖論問(wèn)題,以便更直觀地建模和求解。在加權(quán)有向圖中,變量被表示為頂點(diǎn),約束條件被表示為帶有權(quán)重的有向邊,帶有權(quán)重的有向邊刻畫(huà)了約束條件的取值范圍。如例3所示是一個(gè)簡(jiǎn)單的IDL示例:

例3給定一個(gè)公式φ:

φ=(x-y≤4)∧(x-z>-3)∧(w-x=3)∧(z-y≤2)∧(w-z≤-1)

將公式φ重新改寫(xiě)為φ′:

φ′=(x-y≤4)∧(z-x≤2)∧(w-x≤3)∧(x-w≤-3)∧(z-y≤2)∧(w-z≤-1)

形成的加權(quán)有向圖如圖1所示。加權(quán)有向圖可以非常有效地檢測(cè)差分邏輯的可滿足性,負(fù)循環(huán)用虛線表示。從圖1中可知,x到z到w到x的循環(huán)總權(quán)重為-2,可見(jiàn)公式φ是不滿足的。

Figure 1 Weighted directed graph of example 3圖1 例3的加權(quán)有向圖

3.3 相等理論

給定任何簽名Σ,將包含該理論的所有可能的模型理論表示為T(mén)E,由于對(duì)簽名Σ中符號(hào)的解釋方式?jīng)]有施加任何限制,所以TE也可以稱為未解釋函數(shù)理論EUF(Equality with Uninterpreted Functions)。EUF通常用作一種抽象技術(shù),在許多理論中,決策問(wèn)題可以被歸約到未解釋函數(shù)的決策過(guò)程。給定一個(gè)合取式,其中使用了未解釋函數(shù)項(xiàng)之間的等式,可以使用同余閉包算法[30]來(lái)表示隱含等式的最小集合,這個(gè)表示可以用來(lái)檢查可滿足性。同余閉包算法采用有向無(wú)環(huán)圖DAG(Directed Acyclic Graph)作為數(shù)據(jù)結(jié)構(gòu)。如例4所示為一個(gè)EUF的例子[32]。

例4設(shè)公式:

φ=(f(x)=f(y))∧(x≠y)

3.4 位向量

位向量BV(Bit Vectors)理論是基于位運(yùn)算算法和數(shù)據(jù)結(jié)構(gòu)的理論,用于處理進(jìn)制位的表示和操作。除了標(biāo)準(zhǔn)的算數(shù)運(yùn)算外,位向量還支持混合按位運(yùn)算,比如NOT、AND、OR、XOR以及移位等。它可以用于解決密碼學(xué)哈希函數(shù)反演和數(shù)據(jù)結(jié)構(gòu)位向量操作等問(wèn)題。

3.5 數(shù)組

數(shù)組(Array)理論通常用于對(duì)程序中的實(shí)際數(shù)組進(jìn)行建模,可以被視為對(duì)內(nèi)存的抽象。對(duì)內(nèi)存大小進(jìn)行建模時(shí),使用數(shù)組可以使模型大小與對(duì)內(nèi)存的訪問(wèn)次數(shù)成正比。因此,在建模內(nèi)存時(shí),使用數(shù)組更有效地利用了空間,并獲得了更好的性能。在實(shí)踐中,這種優(yōu)化經(jīng)常產(chǎn)生顯著的效果。例5給出了一個(gè)包含數(shù)組理論的示例。

數(shù)組理論有以下公式[33]定義:對(duì)于?a?i?j?v,有:

read(write(a,i,v),i)=v

i≠j→read(write(a,i,v),j)=read(a,j)

read(i,a)=read(j,a)→i=j

例5給定公式φ=(b-1=c)∧(f(c-b+3)≠f(read(write(a,b,2),c+1))),通過(guò)數(shù)組理論公式簡(jiǎn)單推理得(b-1=c)∧(f(2)≠f(2)),所以公式φ不可滿足。

3.6 組合理論

SMT求解器經(jīng)常涉及到不同理論的相關(guān)符號(hào),需要同時(shí)處理2個(gè)或者2個(gè)以上的理論公式。在這種情況下,需要用到組合理論的求解方法。如果2個(gè)理論Ti和Tj的組合可以簡(jiǎn)單定義為T(mén)i⊕Tj組合而成的理論,在這種理論中往往會(huì)存在一些共享符號(hào),在某一理論下對(duì)共享符號(hào)的解釋會(huì)影響在另一理論下的解釋。因此,將不同理論的約束滿足過(guò)程模塊化地組合成單一過(guò)程,是一個(gè)重要的理論和實(shí)踐問(wèn)題。

1979年Nelson等人[34]提出了經(jīng)典組合理論NO(Nelson-Oppen)判定算法。該算法中任意一階理論是含有等式符號(hào)的自由理論,各個(gè)理論都有自己的判定過(guò)程,各個(gè)理論的簽名兩兩不相交Σi∩Σj=?,且解釋域是無(wú)限的。其判定算法如算法1所示。

算法1 NO判定算法輸入:多理論(T1,…,Ti)公式。輸出:可滿足/不可滿足。步驟1 將輸入的多理論(T1,…,Ti)公式純化為簡(jiǎn)化后的多理論(F1,…,Fi)公式。步驟2 對(duì)每個(gè)理論Ti下的Fi進(jìn)行可滿足性判定。如果返回不滿足,則跳到步驟4。如果推出有關(guān)共享符號(hào)的等式Ei,在存在共享符號(hào)的其他理論Tj(i≠j)下添加Ei,并更新其他理論Tj下的公式Fj,繼續(xù)重復(fù)步驟2直到?jīng)]有新的等式可以傳播。步驟3 如果每個(gè)理論Ti下的公式都可滿足,輸出“可滿足”,結(jié)束算法。步驟4 如果有任意一個(gè)理論Ti下的公式不滿足,輸出“不可滿足”,結(jié)束算法。

純化的目的(如例6)是把組合理論SMT公式分解為統(tǒng)一理論的公式。各理論下的Fi進(jìn)行可滿足性判定。若存在一個(gè)不可滿足,則SMT公式是不可滿足的。各理論中若有共享符號(hào),則進(jìn)行等式傳播。等式傳播是將共享符號(hào)及其等式推出新的等式并添加到此共享符號(hào)的其他理論中。

例6(x1-x2)≤f(x)純化為(x1-x2≤a)∧(a=f(x))。

對(duì)于不相交無(wú)限理論組合方法往往具有指數(shù)級(jí)別的復(fù)雜度。準(zhǔn)確地講,如果Ti的約束滿足問(wèn)題的時(shí)間在O(fi(n))確定,其中i=1,2,則T1⊕T2組合問(wèn)題的時(shí)間可以在O(2n2·(f1(n)+f2(n)))確定[35]。

除了經(jīng)典的組合理論判定算法NO,還有其它算法或在其基礎(chǔ)上改進(jìn)的算法。Nelson等人[36]提出的Ackerman算法主要用于求解含有EUF理論的組合問(wèn)題。Bozzano等人[37,38]提出了Delayed Theory Combination算法和Efficient Theory Combination via Boolean Search算法。前者通過(guò)優(yōu)先考慮布爾分量和每個(gè)理論之間的相互作用,避免了各理論之間的等式傳播過(guò)程,這種算法求解效率比NO算法的高;后者將真值分配的枚舉器與決策過(guò)程集成起來(lái),其關(guān)鍵思想是不僅要搜索公式中出現(xiàn)的原子,還要搜索理論的共享變量之間的所有等式的真值分配,這種算法簡(jiǎn)單而富有表現(xiàn)力。Tinelli等人[39]提出的Combining Non-Stably Infinite Theories算法通過(guò)在組合決策之間傳播等式約束以及最小基數(shù)約束來(lái)解決基于NO算法擴(kuò)展到不穩(wěn)定理論的問(wèn)題,試圖將NO算法提升到不穩(wěn)定無(wú)限理論的相交組合。Zarba等人[40]提出的Combining Sets with Integers算法是在NO算法上的改進(jìn),試圖將NO算法提升到相交理論的組合,主要用于集合和整數(shù)理論的組合域。Barrett等人[41]提出了基于Shostak算法的泛化算法,該算法的核心思想是將不同的理論求解過(guò)程進(jìn)行分解,然后將它們的結(jié)果進(jìn)行合并,從而提高求解效率和準(zhǔn)確性,但此算法的局限性是只適用于一些特定的背景理論,對(duì)于復(fù)雜的組合理論可能無(wú)法有效組合。

3.7 抽象

定義一個(gè)雙射T2B(Theory to Boolean),表示為命題抽象。這個(gè)雙射將Σ的每個(gè)命題符號(hào)映射到本身,將每個(gè)非命題符號(hào)Σ映射到另一個(gè)額外的命題符號(hào),從邏輯上來(lái)講它們是一致的。用B2T(Boolean to Theory)表示T2B的逆,稱為細(xì)化。為了簡(jiǎn)化,常常用φp表示T2B(φ)。如例7所示為抽象的一個(gè)示例:

例7給定公式:

φ=((2x2-x3>2)∨A1)∧((2x3-x4≥5)∨(2x1-x3≤6)∨A1)

抽象為如下命題框架:

φp=T2B(φ)=(B1∨A1)∧(B2∨B3∨A1)

4 SMT判定方法

SMT的判定方法有2種:積極(Eager)方法和惰性(Lazy)方法。Eager方法將SMT公式轉(zhuǎn)換成等價(jià)的SAT公式,并使用SAT求解器求解。Lazy方法則將SAT求解器和理論求解器(T-solver)結(jié)合起來(lái),先將公式抽象為命題公式以得到模型,再檢查模型是否符合理論。表1對(duì)比分析了Eager方法、Lazy方法以及DPLL(T)方法的差異。

4.1 積極方法

SMT求解器通常使用Eager方法[43]將一階邏輯公式轉(zhuǎn)換成命題邏輯形式,這樣可以使用SAT求解器來(lái)判定可滿足性。這種方法將每個(gè)原子公式視為一個(gè)布爾變量,并將不一致性添加到公式中。在調(diào)用SAT求解器之前,Eager方法會(huì)先找出所有的不一致性,這樣可以保證轉(zhuǎn)換后的公式與原始公式具有相同的可滿足性。然而,Eager方法可能會(huì)產(chǎn)生太多的不一致性,導(dǎo)致一個(gè)簡(jiǎn)單的問(wèn)題變得無(wú)法解決。為了避免這種情況,在特定情況下采用不同的編碼策略,比如比特向量的SMT求解器通常使用Eager編碼,以避免生成過(guò)多的不一致性。此外,正確轉(zhuǎn)換每個(gè)理論公式也需要高效的轉(zhuǎn)換過(guò)程,從而提高求解效率。

Eager方法的求解流程大致如下:假設(shè)每個(gè)原子公式都是一個(gè)布爾變量,然后查找所有變量之間的不一致性;接下來(lái)將公式轉(zhuǎn)換成命題邏輯形式;最后將結(jié)果傳遞給SAT求解器并返回結(jié)果。Eager方法的框架[42]如圖2所示。

Eager方法的優(yōu)點(diǎn)是易于設(shè)置和使用,但缺點(diǎn)是可能會(huì)產(chǎn)生太多的不一致性。以下通過(guò)例8來(lái)說(shuō)明算法流程[31]:

Figure 2 Framework of Eager method圖2 Eager方法的框架

例8給定公式:

φ=(x=y)∧(xy)

首先,將每個(gè)原子公式看作一個(gè)命題變量:(x=y)→A,(xy)→C。然后發(fā)現(xiàn),如果x=y,則xy都不能為真。因此,不一致為(A∧B)∧(A∧C)。接著,再將不一致性加入得到命題公式A∧(B∨C)∧(A∧B)∧(A∧C),傳遞給SAT求解器進(jìn)行判定,其返回結(jié)果為不可滿足。因此,公式φ不可滿足,其結(jié)果和SAT求解器返回結(jié)果相同。

4.2 惰性方法

Lazy方法[45]在SAT求解過(guò)程中動(dòng)態(tài)地添加不一致性,因此通常只需要更少的不一致性來(lái)找到解決方案。然而,為了確保Lazy方法正常運(yùn)作,需要與T-solver建立接口,以驗(yàn)證找到的模型滿足理論一致性,這比Eager方法更復(fù)雜。盡管如此,由于其靈活性好,Lazy方法是現(xiàn)有SMT求解器中更常用的方法。Lazy SMT(T)求解方法介紹了一個(gè)SMT求解器依據(jù)Lazy方法來(lái)判定一階邏輯公式的可滿足性。Lazy方法的框架如圖3所示。

算法2很好地描述了基于Offline模式的Lazy SMT(T)的執(zhí)行過(guò)程,Offline模式[30]也被稱為按需引理方法。假定將一個(gè)簽名Σ中的無(wú)量詞

Table 1 Comparison of SMT solution methods表1 SMT求解方法對(duì)比

Figure 3 Framework of Lazy method圖3 Lazy方法的框架

算法2 Lazy SMT(T)判定算法輸入:φ(a QFF in the signature Σ of T)。輸出:sat/unsat。1 Lazy SMT (T-formula φ) {2 φp=T2B(φ);3 while (true) {4 if (DPLL (φp,μp)=="unsat")5 return "unsat";6 else if (T-solver(B2T(μp))=="sat")7 return "sat";8 else9 φp:=φp∧μp;10} }

Figure 4 Process of solving the SMT formula through the Lazy SMT(T) framework圖4 通過(guò)Lazy SMT(T)框架求解SMT公式過(guò)程

公式QFF(Quantifier-Free Formula)φ作為算法的輸入。其求解步驟為:首先,將SMT公式φ通過(guò)T2B抽象為命題公式φp,即公式φ中的項(xiàng)τi視為一個(gè)命題變?cè)?然后,將得到的命題公式φp傳遞給SAT求解器,如果SAT求解器返回不可滿足,則返回不可滿足;如果SAT求解器找到一個(gè)模型μp,將模型μp通過(guò)B2T得到模型μ,通過(guò)理論求解器檢查該模型是否是理論一致的;如果該模型是理論一致的,則返回可滿足;如果該模型是理論不一致的,則將μp作為子句添加到φp中,將生成后的公式傳回SAT求解器,并重新開(kāi)始判定其可滿足性。

Lazy方法的優(yōu)點(diǎn)是提高了求解效率,可擴(kuò)展性強(qiáng),但缺點(diǎn)是不適用于所有類型的問(wèn)題,需要構(gòu)造特定的理論求解器。以下通過(guò)例9來(lái)說(shuō)明Lazy SMT(T)算法流程,圖4為其求解過(guò)程圖。

例9給定公式:

φLIA=(x≥1)∧(x≥1∨x≥3)

SMT公式φ通過(guò)T2B抽象為命題公式,抽象后的命題公式φp=p1∧(p1∨p2)。然后將命題公式傳遞給SAT求解器求解并找到一個(gè)模型μp={p1→false,p2→true}。通過(guò)B2T細(xì)化檢查發(fā)現(xiàn)理論不一致,將p1∧(p1∨p2)∧(p1∨p2)重新傳遞給SAT求解器進(jìn)行求解,返回“不可滿足”,因此SMT公式φLIA是不可滿足的。

4.3 DPLL(T)

不管是Eager方法還是Lazy方法,都是通過(guò)某種策略將SMT公式轉(zhuǎn)化為SAT公式進(jìn)行判定。大多數(shù)現(xiàn)代SAT求解器都是基于DPLL算法框架,SMT也使用了該框架,因?yàn)镾MT求解器依賴SAT求解器來(lái)判定可滿足性。DPLL(T)是一種基于通用DPLL框架的算法,該算法結(jié)合了Eager方法和Lazy方法的優(yōu)點(diǎn)。DPLL(T)算法能夠嵌入許多高效的啟發(fā)式策略,集成不同理論的T-solver。

假定將SMT公式φ和一個(gè)文字集合μ(初始化為?)作為算法的輸入,DPLL(T)內(nèi)嵌的DPLL對(duì)φp和μp進(jìn)行推理和更新。Online模式是比Offline模式更復(fù)雜的模式,算法3給出了基于Online模式[44]的DPLL(T)算法主要過(guò)程。

算法3 DPLL(T)判定算法輸入:φ(a Qff in the signature Σ of T),μ(the set of T- literals)。輸出:sat/unsat。1 DPLL (T-formula φ,T-assigment & μ) {2 if (T-preprocess(φ,μ)=="conflict")3 return "unsat";4 φp=T2B(φ);μp=T2B(μ);5 while (true) {6 T-decide-next-branch (φp,μp);7 while (true) {8 result=T-deduce (φp,μp);9 if (result=="sat") {10 μ=B2T(μp);11 return "sat";}12 else if (result=="conflict") {13 =T-analyze-conflict (φp,μp);14 if (blevel==0)15 return "unsat";16 else T-backtrack (blevel,ηp,φp,μp);}17 else break;18 } } }

例10給定一個(gè)公式φ=(x≥1)∧(A∨(x<1))∧(A∨(x<1))和μ=?。

通過(guò)T-preprocess(φ,μ)將文字(x≥1)重寫(xiě)為(x<1),則φ重寫(xiě)為(x<1)∧(A∨(x<1))∧(A∨(x<1))。然后,根據(jù)布爾約束傳播BCP準(zhǔn)則判定φ是沖突的,因此φ是不可滿足的。

DPLL(T)方法通過(guò)理論預(yù)處理、選擇分支、理論推導(dǎo)、理論沖突分析等操作進(jìn)行改進(jìn),從而提高了求解效率[38,46]。由于其靈活的框架特性,DPLL(T)被許多SMT求解器所采用,例如Z3[17]、CVC5[14]、Yices2[16]、MathSAT5[13]和SMT-RAT[20]等。

5 SMT求解器

近年來(lái),SMT求解器的研究方向主要集中在求解器性能的提高和可擴(kuò)展性的增強(qiáng)上。在性能提高方面,研究人員通過(guò)改進(jìn)底層的數(shù)據(jù)結(jié)構(gòu)、算法和優(yōu)化策略,以及利用并行計(jì)算和GPU加速等技術(shù)來(lái)提高求解速度。增強(qiáng)可擴(kuò)展性方面的研究包括設(shè)計(jì)新的數(shù)據(jù)結(jié)構(gòu)和算法,以支持更多的理論和語(yǔ)言特性。同時(shí),還有研究工作旨在將SMT求解器應(yīng)用于更廣泛的領(lǐng)域,如機(jī)器學(xué)習(xí)、網(wǎng)絡(luò)安全和云計(jì)算等。

為了推動(dòng)SMT研究和SMT求解器的發(fā)展,從2005年開(kāi)始每年都會(huì)舉辦國(guó)際可滿足性模理論競(jìng)賽SMT-COMP(Satisfiability Modulo Theories COMPetition)。表2是目前比較流行的7種求解器的簡(jiǎn)單對(duì)比總結(jié)。圖5是以測(cè)試結(jié)果的排名以及綜合評(píng)分為依據(jù)得到的歷屆SMT-COMP冠軍[48-50]。值得注意的是,比賽從2019年起不再進(jìn)行綜合評(píng)分排名,而是根據(jù)各個(gè)賽道分別進(jìn)行評(píng)分排名。目前主要賽道包括:單查詢(Single Query)、增量查詢(Incremental Query)、Unsat核心(Unsat Core)、模型驗(yàn)證(Model Validation)和并行軌道(Parallel Track)。圖5中2019～2023年所列求解器是在各賽道中獲勝次數(shù)最多的求解器。從圖5可以看出,Z3從2011年到2017年一直保持領(lǐng)先,而最近幾年CVC系列求解器也取得了較好的成績(jī),求解性能非常突出。下面簡(jiǎn)單介紹3個(gè)常見(jiàn)的SMT求解器,分別是Z3、CVC5和MathSAT5。

5.1 Z3求解器

Z3[17]是微軟研究院開(kāi)發(fā)的SMT求解器,使用了類似于MathSAT5的沖突驅(qū)動(dòng)的子句學(xué)習(xí)CDCL(Conflict Driven Clause Learning)算法和策略,同時(shí)支持更多的約束理論和語(yǔ)言。圖6為Z3求解器的體系架構(gòu)[17]。

Figure 5 Championships of previous SMT-COMP圖5 歷屆SMT-COMP的冠軍獲得者

Table 2 Comparison of mainstream SMT solvers

Figure 6 Architecture of Z3圖6 Z3架構(gòu)

首先,使用Simplifier簡(jiǎn)化公式。然后,使用Compiler進(jìn)行處理,將其轉(zhuǎn)換為內(nèi)部數(shù)據(jù)結(jié)構(gòu)和Congruence-Closure節(jié)點(diǎn)。接下來(lái),Congruence-Closure Core接收SAT求解器對(duì)命題公式的賦值,并處理相關(guān)組合理論。由于Z3的體系架構(gòu)易于擴(kuò)展,因此可以根據(jù)需要添加新的邏輯和理論,或改進(jìn)現(xiàn)有算法和數(shù)據(jù)結(jié)構(gòu)。這些改進(jìn)使得Z3在解決各種復(fù)雜問(wèn)題時(shí)表現(xiàn)出色,使其成為目前非常先進(jìn)的求解器之一。

Cai等人[58]突破傳統(tǒng)的算法框架,針對(duì)特定理論提出了首個(gè)局部搜索算法。針對(duì)LIA設(shè)計(jì)了新的算子和評(píng)分函數(shù),提出了新的啟發(fā)式算法,從而開(kāi)發(fā)了特定求解器LS-LIA(Local Search-Linear Integer Arithmetic)。針對(duì)線性實(shí)數(shù)理論和非線性實(shí)數(shù)理論[59],設(shè)計(jì)了新的基于區(qū)間的算子、斷鏈機(jī)制和評(píng)分函數(shù),從而提出了局部搜索算法LS-RA(Local Search-Real Arithmetic)。將這些局部搜索算法和圓柱代數(shù)分解法等加入到Z3求解器中,在Z3求解器的基礎(chǔ)上開(kāi)發(fā)了新的求解器Z3++,使求解性能得到增強(qiáng)。

5.2 CVC5求解器

合作有效性檢查器CVC(Cooperating Validity Checker)系列求解器是一組重要的自動(dòng)定理證明工具,被廣泛應(yīng)用于研究和實(shí)踐中。CVC4[60]是CVC3的重構(gòu)版本,旨在創(chuàng)建一個(gè)更加靈活和高性能的架構(gòu)。CVC5是Barbosa等人[54]開(kāi)發(fā)的SMT求解器,是該系列最新的求解器。它建立在CVC4的代碼基礎(chǔ)和架構(gòu)之上,在性能和功能上都有很大的提升,是目前非常先進(jìn)和高效的SMT求解器之一。CVC5采用了自適應(yīng)的CDCL算法,并支持在廣泛的背景理論及其組合中對(duì)無(wú)量詞和量化公式進(jìn)行推理,包括可滿足性模理論庫(kù)SMT-LIB(Sat- isfiability Modulo Theories LIBrary)[61]中所有標(biāo)準(zhǔn)化的理論。此外,它還原生支持一些非標(biāo)準(zhǔn)理論和理論擴(kuò)展,如分離邏輯、數(shù)列理論、關(guān)系理論和具有超越函數(shù)的實(shí)數(shù)理論擴(kuò)展。圖7為CVC5求解器的體系架構(gòu)[14]。

Figure 7 Architecture of CVC5圖7 CVC5架構(gòu)

CVC5提供了一個(gè)C++API作為主接口,并且在解析器上構(gòu)建了文本命令界面CLI(Command-Line Interface)。其核心引擎是基于CDCL(T)框架的SMT solver模塊。SMT solver模塊由預(yù)處理(Preprocessor)模塊、重寫(xiě)(Rewriter)模塊、命題引擎(Propositional Engine)以及理論引擎(Theory Engine)4個(gè)核心組件組成。預(yù)處理模塊的功能是在進(jìn)行可滿足性檢查前,通過(guò)一系列轉(zhuǎn)換(包括歸一化、簡(jiǎn)化和還原等過(guò)程)對(duì)輸入的公式進(jìn)行預(yù)處理,以保持可滿足性。重寫(xiě)模塊的功能是在求解過(guò)程中將term通過(guò)重寫(xiě)規(guī)則轉(zhuǎn)換為語(yǔ)義等效的規(guī)范形式。命題引擎是CDCL(T)的核心引擎,它接收輸入公式的命題抽象,并在該抽象上產(chǎn)生滿足該公式的模型。理論引擎是負(fù)責(zé)檢查命題引擎,判定理論文字的一致性。除了標(biāo)準(zhǔn)的可滿足性檢查,CVC5還提供了額外的功能,例如歸納、插值、高階推理、語(yǔ)法指導(dǎo)合成SyGuS(Syntax-Guided Synthesis)以及量詞消除。

通過(guò)比較Z3(版本4.8.12)和CVC4(版本1.8)來(lái)評(píng)估CVC5(版本1.0.0)的整體性能。實(shí)驗(yàn)環(huán)境是配置為Intel?CoreTMi5-8265U CPU和8 GB RAM的電腦,在非增量SMT-LIB(2020)基準(zhǔn)測(cè)試實(shí)例中每個(gè)求解器的運(yùn)行截至?xí)r間為1 200 s。實(shí)驗(yàn)結(jié)果如表3,其中#inst表示實(shí)例數(shù)。

Table 3 Results of CVC5/4 and Z3 on SMT-LIB instances表3 CVC5/4和Z3在SMT-LIB實(shí)例上的結(jié)果

通過(guò)實(shí)驗(yàn)分析可知,3種SMT求解器都支持廣泛的理論,且都是目前比較先進(jìn)的求解器?？偟膩?lái)說(shuō),CVC5解決的實(shí)例數(shù)最多,性能好于CVC4的。因?yàn)樘砑恿伺c證明相關(guān)的重構(gòu),CVC5在無(wú)量詞線性算數(shù)中解決的實(shí)例數(shù)相比CVC4的要少。同時(shí),由于位向量求解器還沒(méi)有針對(duì)理論組合進(jìn)行優(yōu)化,CVC5在無(wú)量詞等式位向量中解決的實(shí)例數(shù)比CVC4的要少。此外,在等式線性算數(shù)和無(wú)量詞等式非線性算數(shù)中解決的實(shí)例數(shù)比Z3的少,從而可以針對(duì)這些特定的理論求解進(jìn)行優(yōu)化。

5.3 MathSAT5求解器

MathSAT5是由Cimatti等人[13]開(kāi)發(fā)的SMT求解器,它在支持大多數(shù)SMT-LIB理論及其組合的同時(shí),顯著改進(jìn)了對(duì)增量解法的支持,提供了如Unsat內(nèi)核、插值和ALLSMT等在內(nèi)的許多功能[52]。圖8為MathSAT5求解器的體系架構(gòu)[13]。

Figure 8 Architecture of MathSAT5圖8 MathSAT5架構(gòu)

MathSAT5由Environment和API 2部分組成,在Environment中協(xié)調(diào)求解器中的各個(gè)子組件。預(yù)處理器是一個(gè)term重寫(xiě)引擎,其作用和CVC5重寫(xiě)模塊的相似。編碼器的作用是將一階邏輯公式抽象為CNF命題公式。MathSAT5的核心由SAT引擎和理論求解器組成,它們按照標(biāo)準(zhǔn)的DPLL(T)方法進(jìn)行交互[30]。SAT引擎允許集成外部第三方的高效SAT求解器。理論管理器是SAT引擎和單個(gè)T-solver之間的統(tǒng)一接口,它們只與理論管理器進(jìn)行交互。這樣做的優(yōu)點(diǎn)是T-solver的管理較容易,從而不會(huì)影響系統(tǒng)的其他部分。SAT引擎與理論管理器以及模型或證明器組件進(jìn)行交互,其中后者負(fù)責(zé)生成可滿足公式的模型,并為不可滿足的公式生成反駁證明。

表4為MathSAT5和MathSAT4(版本4.2.17)在SMT-COMP(2009)基準(zhǔn)上的測(cè)試結(jié)果[13]。從結(jié)果中可以明顯得出結(jié)論,即MathSAT5的性能優(yōu)于MathSAT4的性能。

6 SMT的擴(kuò)展及其應(yīng)用

隨著SMT的發(fā)展和深入研究,SMT被應(yīng)用于各種領(lǐng)域,SMT的擴(kuò)展問(wèn)題#SMT也相繼被研究和應(yīng)用。

Table 4 Experimental results of MathSAT4 and MathSAT5表4 MathSAT4和MathSAT5的實(shí)驗(yàn)結(jié)果

6.1 #SMT

在邏輯理論中,#SMT問(wèn)題是一個(gè)復(fù)雜的模型計(jì)數(shù)問(wèn)題,它不僅需要找到一組解來(lái)滿足一階邏輯公式,還需要計(jì)算出滿足該公式的所有解的數(shù)量。由于#SMT問(wèn)題的復(fù)雜度是#P完全的,使得尋找快速且精確的求解算法變得困難。對(duì)于#SMT問(wèn)題,目前大多數(shù)研究都是以LIA、LRA和BV理論為背景的SMT公式的模型計(jì)數(shù)。對(duì)于以線性算數(shù)為背景理論的#SMT問(wèn)題,可以將其轉(zhuǎn)化為計(jì)算一階邏輯公式所形成的凸面體的體積。而對(duì)于以位向量理論為背景的#SMT問(wèn)題,大多采用基于哈希的模型計(jì)數(shù)近似方法[62]。

Ma等人[63]在早期提出了一種精確求解小規(guī)模線性問(wèn)題計(jì)數(shù)的方法,但該方法并不適用于大規(guī)模問(wèn)題。周俊萍等人[12]針對(duì)線性算數(shù)理論提出了一種基于局部搜索算法求解大規(guī)模#SMT問(wèn)題的近似算法。該算法基于DPLL(T)框架,通過(guò)使用群體規(guī)則減少計(jì)算體積的次數(shù),再通過(guò)一種差分進(jìn)化方法[64,65]枚舉各個(gè)有解域,從而提高求解效率。Chistikov等人[66]提出了一種以LIA和LRA為背景理論的SMT公式的模型計(jì)數(shù)算法,該算法能夠給出具有近似誤差形式邊界的近似解。Borges等人[67]總結(jié)了適用于復(fù)雜非線性約束的模型計(jì)數(shù)技術(shù),指出最有實(shí)用性的技術(shù)是近似模型計(jì)數(shù)和位級(jí)哈希。Ge等人[68]提出了一個(gè)計(jì)算和估計(jì)線性算數(shù)理論約束解空間體積大小的工具VolCE(Volume Computation and Estimation),該工具可以計(jì)算和估算LRA公式形成的凸面體的體積,統(tǒng)計(jì)LIA公式位于解空間的樣本點(diǎn)。由于VolCE使用了高效的啟發(fā)式算法,對(duì)于大規(guī)模的LRA公式也可以高精度地進(jìn)行體積估計(jì)。Gao等人[69]提出了用馬爾科夫鏈蒙特卡洛抽樣策略估計(jì)以LIA為約束條件的解空間體積的近似方法,該方法和其他先進(jìn)方法相比具有競(jìng)爭(zhēng)力且有較好的可擴(kuò)展性。Kim等人[70]提出了一種結(jié)構(gòu)近似模型計(jì)數(shù)算法用于結(jié)構(gòu)位向量模型計(jì)數(shù)。該算法通過(guò)分析SMT公式結(jié)構(gòu)以確定其解個(gè)數(shù)的上下界,且不依賴于決策過(guò)程。基于此算法構(gòu)建了SMC(Structural Model Counter)計(jì)數(shù)器,通過(guò)對(duì)比其他先進(jìn)近似模型計(jì)數(shù)器,驗(yàn)證了該算法是一個(gè)快速的多項(xiàng)式算法。

Ge等人[71]于2019年提出并證明了線性約束條件下通過(guò)空間量化近似整數(shù)計(jì)數(shù)的理論邊界,通過(guò)理論分析提出了一種線性約束的近似整數(shù)解計(jì)數(shù)方法,并基于此方法提出了近似整數(shù)計(jì)數(shù)器。此方法首先應(yīng)用高斯消元減少等式,然后通過(guò)線性規(guī)劃計(jì)算Mi(P)和mi(P),并通過(guò)式(2)計(jì)算誤差err。最后通過(guò)體積計(jì)算工具和體積估計(jì)工具輸出近似值、下界和上界組成的三元組。通過(guò)實(shí)驗(yàn)分析可知,此方法可擴(kuò)展性強(qiáng)且非常高效。

(2)

隨后,Ge等人[72]又提出了一種新的整數(shù)計(jì)數(shù)方法,該方法利用基于列消去和行消去的分解技術(shù),進(jìn)一步提高了整數(shù)計(jì)數(shù)算法的性能。該方法首先消除選擇的行和列得到新約束;接著,再?gòu)男录s束中確定所有的連通分量,這些分量對(duì)應(yīng)不同的變量集、子矩陣和子向量;然后,問(wèn)題P可以被分為k個(gè)子問(wèn)題,進(jìn)而將線性約束的整數(shù)計(jì)數(shù)問(wèn)題分解為獨(dú)立的子問(wèn)題?；谠摲椒ㄌ岢隽薎ntcount計(jì)數(shù)器,采用來(lái)自程序分析和簡(jiǎn)單時(shí)間規(guī)劃的基準(zhǔn)[71],與先進(jìn)的整數(shù)計(jì)數(shù)器Barvinok進(jìn)行對(duì)比,結(jié)果如圖9所示[72]。圖9中,橫縱坐標(biāo)均代表計(jì)數(shù)器的運(yùn)行時(shí)間?？梢钥闯?IntCount在一定時(shí)間內(nèi)能處理更多的實(shí)例,可見(jiàn)該分解計(jì)數(shù)方法在擴(kuò)展計(jì)數(shù)器能力上是非常高效的。

Figure 9 Performance comparison of IntCount and Barvinok on benchmarks圖9 IntCount和Barvinok在基準(zhǔn)上的性能比較

#SMT問(wèn)題的解決在軟硬件形式化驗(yàn)證、人工智能等多個(gè)領(lǐng)域有著重要的應(yīng)用意義。在軟件測(cè)試領(lǐng)域,可以使用#SMT問(wèn)題生成具有特定屬性的測(cè)試用例。在人工智能領(lǐng)域,#SMT可以用于解決資源分配、路徑規(guī)劃等問(wèn)題。#SMT在加密和區(qū)塊鏈領(lǐng)域也有廣泛的應(yīng)用,它可以用于驗(yàn)證加密算法的安全性,檢測(cè)密碼破解的可能性,并對(duì)加密協(xié)議和區(qū)塊鏈智能合約提供形式化分析。為了解決#SMT問(wèn)題,研究人員已經(jīng)開(kāi)發(fā)了許多基于啟發(fā)式方法的求解器。盡管這些求解器在實(shí)踐中已經(jīng)取得了一定的成功,但在處理大規(guī)模問(wèn)題時(shí)仍然面臨著計(jì)算效率和精度的挑戰(zhàn)。

6.2 SMT在深度神經(jīng)網(wǎng)絡(luò)中的應(yīng)用

近些年,一些技術(shù)[73]已經(jīng)將求解器集成到深度神經(jīng)網(wǎng)絡(luò)DNNs(Deep Neural Networks)中。這些技術(shù)展示了歸納學(xué)習(xí)和符號(hào)推理技術(shù)之間搭建橋梁的前景。這類技術(shù)在訓(xùn)練過(guò)程和推理過(guò)程中均可使用。Wang等人[74]提出了一種可以集成到DNNs中的可微MAXSAT層,該層采用快速坐標(biāo)下降法高效計(jì)算前向和后向通道。Vlastelica等人[75]將求解器與深度學(xué)習(xí)結(jié)合起來(lái),以解決原始輸入數(shù)據(jù)上的組合問(wèn)題。

Fredrikson等人[76]提出了一套將SMT求解器集成到DNNs的前向和后向通道的方法,被稱為SMTLayer。通過(guò)這種方法,可以將豐富的領(lǐng)域知識(shí)以數(shù)學(xué)公式的形式編碼到神經(jīng)網(wǎng)絡(luò)中。SMTLayer是一套用于計(jì)算層的前向和后向傳遞算法,其行為由一組用戶定義的SMT約束來(lái)確定。SMTLayer不包含可訓(xùn)練的參數(shù),而是完全依賴于模型設(shè)計(jì)者提供的一組SMT約束φ來(lái)定義其功能。SMTLayer主要用于DNNs的頂部,從傳統(tǒng)DNNs層的堆棧中獲取輸入,將原始輸入特征轉(zhuǎn)換為嵌入SMTLayer的約束條件φ(z0,…,zp-1,y0,…,yq-1)的項(xiàng),并產(chǎn)生與φ和給定項(xiàng)一致的輸出。圖10是一個(gè)MNIST加法示例[73]。

Figure 10 Example of MNIST addition圖10 MNIST加法示例

算法4給出了前向傳遞算法的基本框架。在前向傳遞[76]過(guò)程中,對(duì)φ的限制是z和y必須是布爾值的向量。除此之外,φ中出現(xiàn)的其它符號(hào)可以是來(lái)自底層SMT求解器支持的任意域。

算法4 基于SMTLayer的前向傳遞算法輸入:前一層的輸出z0,…,zp-1,公式φ(z0,…,zp-1,y0,…,yq-1)。輸出:浮點(diǎn)值y0,…,yq-1。步驟1 在φ中替換zi的基本項(xiàng),構(gòu)建公式^φ。步驟2 判定^φ是否可滿足。如果可滿足,跳到步驟3;如果不可滿足,跳到步驟4。步驟3 獲取求解器模型y0,…,yq-1,通過(guò)將false映射為-1,true映射為1,輸出浮點(diǎn)值y0,…,yq-1。步驟4 輸出y值0。

算法5給出了后向傳遞算法的基本框架。在后向傳遞[76]過(guò)程中,可以找到輸出損失更小的輸入特征,并且通過(guò)將這些特征的梯度傳回到前面的層來(lái)進(jìn)行參數(shù)更新,以優(yōu)化神經(jīng)網(wǎng)絡(luò)并降低損失函數(shù)值。

算法5 基于SMTLayer的后向傳遞算法輸入:前向傳遞的輸入和輸出,二元交叉熵?fù)p失函數(shù)l(y,y*)的梯度,公式φ(z0,…,zp-1,y0,…,yq-1)。輸出:梯度Gz。步驟1:使用梯度、輸入和輸出計(jì)算修正后的輸出^y,該輸出對(duì)應(yīng)損失更小的輸出;步驟2:使用^y判定輸入中哪些分量與φ和^y不一致,通過(guò)梯度計(jì)算的方法計(jì)算梯度Gz;步驟3:向前一層輸出相應(yīng)的梯度Gz。

綜上,SMTLayer是一個(gè)將SMT求解器集成到DNNs中的方法,使用SMTLayer可以降低對(duì)訓(xùn)練數(shù)據(jù)的依賴,提高訓(xùn)練效率,并且表現(xiàn)得非常健壯。

6.3 SMT求解器與量子計(jì)算的結(jié)合

隨著量子技術(shù)的迅猛發(fā)展,驗(yàn)證量子程序的正確性、優(yōu)化量子編譯過(guò)程以及診斷量子系統(tǒng)中的錯(cuò)誤變得越來(lái)越具有挑戰(zhàn)性。為了應(yīng)對(duì)這些挑戰(zhàn),研究人員開(kāi)始探索將SMT求解器與量子技術(shù)相結(jié)合的方法。

Deng等人[78]提出了量子程序的元編程框架MQCC(Meta Quantum Circuits with Constraints),通過(guò)MQCC的編譯器生成合適的約束,再結(jié)合SMT求解器求解,生成優(yōu)化的、可運(yùn)行的程序。Seino等人[79]提出了一種基于SMT求解器的量子電路綜合方法,該方法由CNOT(Control-NOT)門(mén)、H(Hadamard)門(mén)和T門(mén)組成,滿足NNA(Nearest Neighbor Architecture)限制。該方法通過(guò)處理量子特定的T門(mén)和H門(mén)的功能,利用Z3求解器最大限度地減少CNOT門(mén)的數(shù)量。Murali等人[80]提出了一種Scaffold量子編程語(yǔ)言的編譯器,其中的優(yōu)化是專門(mén)針對(duì)具有數(shù)百個(gè)量子比特的噪聲中尺度量子NISQ(Noisy Intermediate-Scale Quantum)機(jī)器。編譯器從Scaffold程序中提取門(mén),并構(gòu)建一個(gè)同時(shí)考慮程序特性和機(jī)器約束的約束優(yōu)化問(wèn)題。然后,使用Z3求解器將程序量子比特映射到硬件量子比特、調(diào)度門(mén)(Gate Scheduling)和CNOT路由門(mén)(CNOT Routing),進(jìn)而減少整體執(zhí)行時(shí)間。

量子SMT求解器是將量子技術(shù)與SMT結(jié)合起來(lái)開(kāi)發(fā)的求解器。Lin等人[81]提出了基于量子算法Grover[82]的BV理論的量子SMT求解器。其利用量子系統(tǒng)中疊加和糾纏的性質(zhì),使求解器能夠同時(shí)考慮所有的輸入,并在一次迭代中檢驗(yàn)它們?cè)诓紶栍蚝屠碚撚蛑g的一致性。量子SMT求解器的整體框架如圖11所示。整體架構(gòu)由4個(gè)部分組成。

Figure 11 Overall framework of quantum SMT solver圖11 量子SMT求解器整體框架

SAT Circuit的作用是確定布爾域的解。Theory Circuit的作用是確定理論是否是一致的、不沖突的。Consistency Extractor的作用是結(jié)合量子系統(tǒng)來(lái)識(shí)別布爾域和理論域都一致的解。Solution Inverser的作用是反推SMT公式的解。

綜上,SMT求解器作為一種強(qiáng)大的自動(dòng)推理工具,可以將量子問(wèn)題轉(zhuǎn)化為SMT約束來(lái)解決復(fù)雜的約束問(wèn)題,也可以將SMT求解器與量子計(jì)算相結(jié)合來(lái)開(kāi)發(fā)出量子SMT求解器,從而提高求解器的求解速度以及發(fā)現(xiàn)所有解的能力。這種結(jié)合對(duì)量子領(lǐng)域發(fā)展和提高SMT求解器性能均提供了新的可能性。

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

近年來(lái),隨著計(jì)算機(jī)硬件的不斷發(fā)展和計(jì)算能力的提高,SMT領(lǐng)域取得了一些重要進(jìn)展。然而,SMT在實(shí)際應(yīng)用中仍然面臨著諸多挑戰(zhàn)。一方面,SMT需要求解更復(fù)雜的邏輯公式(例如包含量詞的公式),求解效率和可擴(kuò)展性是其主要的瓶頸。另一方面,SMT的求解精確性和容錯(cuò)能力也是關(guān)鍵,特別是當(dāng)邏輯公式不完整、不一致或含有錯(cuò)誤時(shí),需要更加精確、健壯的算法和求解器來(lái)解決問(wèn)題。未來(lái),SMT可以在以下幾個(gè)方面得到進(jìn)一步的研究和發(fā)展:

(1)隨著機(jī)器學(xué)習(xí)技術(shù)的發(fā)展,可以將SMT和機(jī)器學(xué)習(xí)算法結(jié)合,以解決更加復(fù)雜和龐大的問(wèn)題。

(2)隨著SMT應(yīng)用范圍的不斷擴(kuò)大,提高SMT求解器的效率和速度成為了研究重點(diǎn)。未來(lái)的研究將致力于針對(duì)特定背景理論開(kāi)發(fā)更加高效的求解器。

(3)#SMT具有較高的計(jì)算復(fù)雜性,在最壞情況下可能需要指數(shù)級(jí)時(shí)間。為降低計(jì)算復(fù)雜性,需研究更高效、通用且可擴(kuò)展的算法,以適應(yīng)不同類型和規(guī)模的#SMT。同時(shí),加強(qiáng)#SMT的理論研究,如復(fù)雜性分析和算法正確性證明,也有助于設(shè)計(jì)更有效的解決方案。

(4)隨著量子技術(shù)的發(fā)展,SMT也將面臨新的挑戰(zhàn)和機(jī)遇。未來(lái)的研究將探索SMT與量子算法相結(jié)合,擴(kuò)展到其他更多理論,以加快求解效率和提高求解精度。

總之,本文從SMT出發(fā),總結(jié)了背景理論、求解方法、求解器、擴(kuò)展問(wèn)題和最新應(yīng)用。對(duì)于SMT的求解還有非常大的研究和發(fā)展空間。未來(lái)的研究將致力開(kāi)發(fā)更加精確和高效的算法和求解器,并將其應(yīng)用于更多的領(lǐng)域以解決實(shí)際問(wèn)題。