可滿足性模理論綜述*

唐 傲,王曉峰,2,何 飛

(1.北方民族大學計算機科學與工程學院,寧夏 銀川 750021; 2.北方民族大學圖像圖形智能處理國家民委重點實驗室,寧夏 銀川 750021)

1 引言

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

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

2 基本概念和定義

SMT問題是判定帶有背景理論的一階邏輯公式的可滿足性問題。這些理論包括數(shù)學理論和計算機領域中的數(shù)據(jù)結構理論等。一階邏輯是一種比命題邏輯更強大的邏輯體系,它擴展了命題邏輯,并引入了可量化的變量。一階邏輯公式由非邏輯符號和邏輯連接符組成,其中非邏輯符號包括命題變元和常元、個體變元和常元、謂詞變元和常元以及函數(shù)變元和常元。一個一階邏輯,如果它包括一系列可量化的變元、一個或多個有意義的謂詞符號,由一組包含有意義的謂詞符號的公理所組成,針對特定的論域進行建模,那么它就是一個一階理論。這些特性使得一階邏輯非常適合用于描述復雜的邏輯問題。

2.1 命題邏輯

例1給定一個命題公式:

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

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

2.2 一階邏輯

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

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

(2)f∈ΣF是一個形式為δ1×δ2×…×δn→δ的n元函數(shù),當n=0時,f是一個常量符號。

(3)p∈ΣP是一個形式為δ1×δ2×…×δn→δ的n元謂詞,當n=0時,p是一個命題符號。

(4)在變量集合ΣX中,每個變量與S中的一個類型δi對應。

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

(1)若x∈ΣX是具有類型δ的變量,且x為個體變元或個體常元,則x∈term;

(2)若f(t1,t2,…,tn)∈ΣF,n≥0,是具有類型δ的函數(shù),f為n元函數(shù)變元或常元,其中ti(1≤i≤n,n∈N+)為項,則f(t1,t2,…,tn)∈term。當n=0時,f稱為個體變元或個體常元;

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

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

若p(t1,t2,…,tn)∈ΣP是n元謂詞,n≥0,p為n元謂詞變元或常元,其中ti(1≤i≤n,n∈N+)為項,則p(t1,t2,…,tn)稱為原子公式。當n=0時,p稱為命題變元或命題常元。

定義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ī)則(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+)為項,p為n元謂詞變元。

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

公式φ中一個項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 常見背景理論

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

3.1 線性算數(shù)

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

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

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

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

(3)Σiaixi

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

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

需要注意的是,在算數(shù)理論中引入乘法會大大增加問題的復雜性,因此在實踐中通常會避免使用?；竟降暮先》妒皆谡麛?shù)情況下會變得無法判定。雖然在實際情況下是可判定的,但其復雜度會達到雙指數(shù)級別。然而,在建模和推理系統(tǒng)時,算數(shù)理論非常有用,尤其是在建模有限集合、程序算數(shù)、指針和內存操作等方面。因此,盡管存在一些復雜性問題,仍然需要在實踐中使用算數(shù)理論去解決特定問題。如例2所示是一個典型的LA公式φ:

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

3.2 差分邏輯

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

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

例3給定一個公式φ:

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

將公式φ重新改寫為φ′:

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

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

Figure 1 Weighted directed graph of example 3圖1 例3的加權有向圖

3.3 相等理論

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

例4設公式:

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

3.4 位向量

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

3.5 數(shù)組

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

數(shù)組理論有以下公式[33]定義:對于?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))),通過數(shù)組理論公式簡單推理得(b-1=c)∧(f(2)≠f(2)),所以公式φ不可滿足。

3.6 組合理論

SMT求解器經常涉及到不同理論的相關符號,需要同時處理2個或者2個以上的理論公式。在這種情況下,需要用到組合理論的求解方法。如果2個理論Ti和Tj的組合可以簡單定義為Ti⊕Tj組合而成的理論,在這種理論中往往會存在一些共享符號,在某一理論下對共享符號的解釋會影響在另一理論下的解釋。因此,將不同理論的約束滿足過程模塊化地組合成單一過程,是一個重要的理論和實踐問題。

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

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

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

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

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

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

3.7 抽象

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

例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公式轉換成等價的SAT公式,并使用SAT求解器求解。Lazy方法則將SAT求解器和理論求解器(T-solver)結合起來,先將公式抽象為命題公式以得到模型,再檢查模型是否符合理論。表1對比分析了Eager方法、Lazy方法以及DPLL(T)方法的差異。

4.1 積極方法

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

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

Eager方法的優(yōu)點是易于設置和使用,但缺點是可能會產生太多的不一致性。以下通過例8來說明算法流程[31]:

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

例8給定公式:

φ=(x=y)∧(xy)

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

4.2 惰性方法

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

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

Table 1 Comparison of SMT solution methods表1 SMT求解方法對比

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 通過Lazy SMT(T)框架求解SMT公式過程

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

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

例9給定公式:

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

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

4.3 DPLL(T)

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

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

算法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給定一個公式φ=(x≥1)∧(A∨(x<1))∧(A∨(x<1))和μ=?。

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

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

5 SMT求解器

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

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

5.1 Z3求解器

Z3[17]是微軟研究院開發(fā)的SMT求解器,使用了類似于MathSAT5的沖突驅動的子句學習CDCL(Conflict Driven Clause Learning)算法和策略,同時支持更多的約束理論和語言。圖6為Z3求解器的體系架構[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架構

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

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

5.2 CVC5求解器

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

Figure 7 Architecture of CVC5圖7 CVC5架構

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

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

Table 3 Results of CVC5/4 and Z3 on SMT-LIB instances表3 CVC5/4和Z3在SMT-LIB實例上的結果

通過實驗分析可知,3種SMT求解器都支持廣泛的理論,且都是目前比較先進的求解器?？偟膩碚f,CVC5解決的實例數(shù)最多,性能好于CVC4的。因為添加了與證明相關的重構,CVC5在無量詞線性算數(shù)中解決的實例數(shù)相比CVC4的要少。同時,由于位向量求解器還沒有針對理論組合進行優(yōu)化,CVC5在無量詞等式位向量中解決的實例數(shù)比CVC4的要少。此外,在等式線性算數(shù)和無量詞等式非線性算數(shù)中解決的實例數(shù)比Z3的少,從而可以針對這些特定的理論求解進行優(yōu)化。

5.3 MathSAT5求解器

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

Figure 8 Architecture of MathSAT5圖8 MathSAT5架構

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

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

6 SMT的擴展及其應用

隨著SMT的發(fā)展和深入研究,SMT被應用于各種領域,SMT的擴展問題#SMT也相繼被研究和應用。

Table 4 Experimental results of MathSAT4 and MathSAT5表4 MathSAT4和MathSAT5的實驗結果

6.1 #SMT

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

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

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

(2)

隨后,Ge等人[72]又提出了一種新的整數(shù)計數(shù)方法,該方法利用基于列消去和行消去的分解技術,進一步提高了整數(shù)計數(shù)算法的性能。該方法首先消除選擇的行和列得到新約束;接著,再從新約束中確定所有的連通分量,這些分量對應不同的變量集、子矩陣和子向量;然后,問題P可以被分為k個子問題,進而將線性約束的整數(shù)計數(shù)問題分解為獨立的子問題。基于該方法提出了Intcount計數(shù)器,采用來自程序分析和簡單時間規(guī)劃的基準[71],與先進的整數(shù)計數(shù)器Barvinok進行對比,結果如圖9所示[72]。圖9中,橫縱坐標均代表計數(shù)器的運行時間?？梢钥闯?IntCount在一定時間內能處理更多的實例,可見該分解計數(shù)方法在擴展計數(shù)器能力上是非常高效的。

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

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

6.2 SMT在深度神經網(wǎng)絡中的應用

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

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

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

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

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

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

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

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

6.3 SMT求解器與量子計算的結合

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

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

量子SMT求解器是將量子技術與SMT結合起來開發(fā)的求解器。Lin等人[81]提出了基于量子算法Grover[82]的BV理論的量子SMT求解器。其利用量子系統(tǒng)中疊加和糾纏的性質,使求解器能夠同時考慮所有的輸入,并在一次迭代中檢驗它們在布爾域和理論域之間的一致性。量子SMT求解器的整體框架如圖11所示。整體架構由4個部分組成。

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

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

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

7 結束語

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

(1)隨著機器學習技術的發(fā)展,可以將SMT和機器學習算法結合,以解決更加復雜和龐大的問題。

(2)隨著SMT應用范圍的不斷擴大,提高SMT求解器的效率和速度成為了研究重點。未來的研究將致力于針對特定背景理論開發(fā)更加高效的求解器。

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

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

總之,本文從SMT出發(fā),總結了背景理論、求解方法、求解器、擴展問題和最新應用。對于SMT的求解還有非常大的研究和發(fā)展空間。未來的研究將致力開發(fā)更加精確和高效的算法和求解器,并將其應用于更多的領域以解決實際問題。