一種結合CCgscore算法的SMT求解技術*

連召洋，靳慶庚，谷 濤，吳 昊

（廣西民族大學廣西混雜計算與集成電路設計分析重點實驗室，南寧　530006）

一種結合CCgscore算法的SMT求解技術*

連召洋，靳慶庚，谷 濤，吳 昊

（廣西民族大學廣西混雜計算與集成電路設計分析重點實驗室，南寧530006）

提出了對SMT問題的另一種方法.首先，編譯SMT公式并轉換為CNF公式.然后充分借鑒求解SAT問題中所用的方法，把它和SMT理論相結合，借鑒在2014SAT競賽中的CCgscore算法，得到一個滿足CNF公式的解.最后把得到的當前解與T－solver進行交互并且檢查其在特定理論背景下的可滿足性.由于在SMT求解的過程中結合了先進的CCgscore算法，所以在求解某些SMT問題時效果比較好.

CCgscore；可滿足性模理論；Lazy；格局配置

0　引言

The SMT（Satisfiability Modulo Theories）可滿足模理論[1－4]可以求解一階邏輯相關的公式，其中公式的謂詞變量和函數變量都是基于某一特定領域的理論，因此，它可以彌補SAT問題在表達能力上的不足.SAT求解器[5]只能解決布爾可滿足問題的，只涉及命題邏輯，但是SMT求解器可以解決涉及抽象函數等式（Equality with Uninterpreted Functions，EUF）、差分算術（Diference Arithmetic）、位向量（Bit Vector，BV）、數組（Arrays）等理論的問題.現在，已經開發出了很多高效的SMT求解器，從最早的Eager框架[4]到主流的LAZY框架[3－4]，其中Eager框架是把SMT公式完全轉換為SAT公式，然后調用SAT求解器，而不考慮具體的理論，不調用理論求解器.LAZY框架則致力于設計一些SMT求解器，去判定在特定理論下子句集的可滿足性.筆者選擇在LAZY框架下，結合現成主流SAT算法去改進SMT的去解問題.在文章中借鑒了在2014SAT競賽中的CCgscore算法.

1　CCgscore算法

SAT求解器的本地搜索策略是選擇一個變量進行翻轉并進行判斷，努力去發現一個可以滿足的一組賦值.一個求解器的本地搜索的本質部分是采用啟發式策略去選擇變量.CCgscore[6]是一種局部搜索求解器，它主要有兩個理念.第一個[7]是提出的格局檢查（CC）策略，這個方法已經被應用于解決CC最小頂點覆蓋問題[8]，然后到SAT問題[9]，根據對于SAT問題中的CC策略，一個變量χ是格局改變當且僅當在變量χ翻轉之后，變量χ的鄰接變量中，至少有一個發生翻轉.在貪婪模式中，CC策略通常允許格局改變過的變量進行翻轉.CCgscore的第二個理念是引用一個混合評分函數，叫廣義評分，記作gscore.隨后，又提出多級屬性的概念，比如把score的二級屬性記作score2，make的二級屬性記作make2，對于解決長子句的隨機k－sat問題非常有效.這個gscore函數被定義為：

2　結合CCgcore算法的新SMT求解器

2.1新算法的基本流程

2.1.1編譯并轉化SMT公式

首先，根據smt2文件讀取SMT公式，然后對其進行解析和設置命令，接著對其用Egraph圖進行存儲，其中對SMT公式中每個基本的單元，并用Enode來存儲，然后根據Tseitin變換再對其CNF化，并對CNF化后產生的新結點重新用Egraph進行存儲.例如：

一個SMT公式如下：

經過轉換后由上述SMT公式得到的CNF公式為

其中Egraph圖中結點Enode中代表的內容和CNF化后命題變量的對應關系為：

其中CNF＿54＿45、CNF＿54＿51、CNF＿51＿45是進行CNF化后產生的新結點.P3、P8、P9分別代表產生的新結點對應的命題變量.

2.1.2調用CCgscore算法

采用CCgscore算法對2.1.1中產生的公式進行求解，如果超時則重復調用CCgscore算法，如果重復超一定次數，則整個程序結束返回SAT＿UNKONWN.如果找到一組可滿足的解則返回SAT＿SAT，并且進行2.1.3.

CCgscore算法的偽代碼為：

1）If?格局變化過的變量，并且score（χ）＞0或者score（χ）＞st那么

2）Return總評分值最大的變量；其中總評分為：

3）更新子句的權重；其中權重為：

4）隨機的從在滿足的子句中選擇一個子句c；

5）Return一個在子句c中總評分最大的變量；

2.1.3與理論求解器進行交互

根據2.1.2中所得到的解，驗證在具體的理論下的可滿足性.如果滿足，那么說明這個SMT公式可滿足程序結束并返回SMT＿SAT；如果驗證后不滿足，那這個SMT公式就返回SMT＿UNSAT并重復調用2.1.2；如果驗證超時那么就返回SMT＿UNKONWN.

2.2新算法的框圖

圖1　算法框架圖Fig.1　The figure of algorithm frame

3　實驗結果

實驗環境平臺：UBUNTU 13.10，CPU：Inter（R）i3－M390CPU@2.67GHZ，RAM：3GB.

在這個實驗中筆者測試了SMT的Benchmarks，對每個實例在60s內進行了20次測試，這里的運行時間都是每個實例這20次中最優級的，也就是用時最少的.我們得到了一些好的結果.如表1所示，結果顯示結合CCgscore算法改進SMT問題的求解CCGSMT是可行的，并且在一些SMT Benchmarks的測試上也有一些好的效果.

表1　實驗結果Tab.1　Experiment result

圖2橫軸為變量數，縱軸為CCGSMT的運行時間.此圖顯示了結合CCgscore算法的新的CCGSMT的運行時間，隨變量個數變化的關系.由圖2可知基本上是呈螺旋狀上升的關系.

圖2　運行時間與變量數的關系Fig.2　The relation between runtime and the number of variables

圖3橫軸為子句數，縱軸為CCGSMT的運行時間.此圖顯示了結合CCgscore算法的新的CCGSMT的運行時間，隨子句個數變化的關系.由圖3可知基本上也是呈螺旋狀上升的關系.

圖3　運行時間與子句數的關系Fig.3　The relation between runtime and the number of clauses

[1]Mnacho Echenim，Nicolas Peltier.A New Instantiation Scheme for Satisfiability Modulo Theories[J].JAR，2012，48：293－362.

[2]Anping He，Daoshe Lu，Jinzhao Wu.A SMT Solver Based on Anthropomo－rphic and Quasi－Physical[C].ICACC′13，2013.

[3]Roberto S.Lazy Satisfiability Modulo Theories[J].JSAT，2007（3）：141－224.

[4]Armin B，Marijn H，Hans V，et al.Handbook of Satisfiability [M].IOS Press，2009：825－886.

[5]Matthew W.Moskewicz，Conor F.Madigan，Ying Zhao，Linao Zhang.Engineering an Efficient SAT Solver[C].In 38th DAC，pages 530－535，Las Vages，NV，June 2001.

[6]Li C，Li J，Wu Y.CCA2014：A Local Search Solver for the SAT Problem[J].SAT COMPETI－TION 2014：16.

[7]S.Cai，K.Su，and A.Sattar.Local search with edge weighting and configuration checking heuristics for minimum vertex cover[J]. Artificial Intelligence.，2011，175（9－10）：1672－1696.

[8]S.Cai and K.Su.Two new local search strategies for minimum vertex cover[C].inProc.ofAAAI，2012：441－447.

[9]S.Cai and K.Su.Configuration checking with aspiration in local search for SAT[C].inProc.ofAAAI，2012：434－440.

[責任編輯 蘇 琴]

[責任校對 黃祖賓]

A New SMT Solver Combined with CCgscore Algorithm

LIAN Zhao－yan，JIN Qing－geng，GU Tao，WU Hao
（Guangχi Key Laboratory of Hybrid Computation and IC Design Analysis，Guangχi University for Nationalities，Nanning530006，China）

This paper presents another method for the SMT problem.First of all，compile the SMT formula and convert it to CNF formula.Then make full use of method for solving SAT problem，and combine it with the theory of SMT.In this paper draws，it combine the CCgscore algorithm in the 2014SAT race，to get a satisfied solution of CNF formula.Finally，the current solution interacts with T－solver and check whether satisfied in particular theory background.Because the new algorithm combine the advanced CCgscore algorithm into solving of SMT problem，so it is more efficient in solving certain type of SMT problem.

CCgscore；SMT；LAZY；CC3

TP301.6

A

1673－8462（2015）02－0066－03

2015－03－05.

廣西研究生教育創新計劃項目資助（No.YCSZ2014121）.

連召洋（1989－），男，河南平頂山人，廣西民族大學碩士研究生，研究方向：形式化驗證.