一种快速低内存消耗的SMT全解求解器  

A Fast and Low Memory Consumption All-SMT Solver

作　　者：白杨 贾悠 BAI Yang;JIA You(No.30 Institute of CETC,Chengdu Sichuan 610041,China;School of Computer Science and Engineering,University of Electronic Science and Technology of China,Chengdu Sichuan 611731,China)

机构地区：[1]中国电子科技集团公司第三十研究所,四川成都610041 [2]电子科技大学计算机科学与工程学院(网络空间安全学院),四川成都611731

出　　处：《通信技术》2020年第7期1623-1629,共7页Communications Technology

摘　　要：SMT全解求解器为许多研究领域提供辅助,但现有的SMT全解求解器在速度、内存消耗或者支持的求解类型方面存在局限性。首先,提出了求解器的4种新的潜在应用;其次,设计了一种基于二分查找(Binary Search,BS)的新型求解器,可以支持多种求解类型,同时,结合上下文感知(Context Aware,CA)机制来提升求解器的速度,并通过暂停恢复(Suspend Resume,SR)机制降低内存消耗。初步试验表明,BS、BS+CA、BS+SR和所提方法分别能将传统的阻塞子句方法(Blocking Clauses Method,BCM)的求解速度提高了4.6倍、13.4倍、7.3倍以及32.4倍;与BCM相比,提出的方案的内存消耗降低至35.3%。此外,试验结果表明,可以通过并行化进一步提升方案的性能。The All-SMT solver provides assistance for many research fields,but the existing All-SMT solver has limitations in speed,memory consumption or supported solution types.Firstly,four new potential applications of the solver are proposed.Then,a new solver based on BS(Binary Search)is designed,which can support multiple solution types.At the same time,combined with the CA(Context Aware)mechanism,the speed of the solver is improved,and through the SR(Suspend Resume)mechanism,the memory consumption reduced.Preliminary experiments indicate that BS,BS+CA,BS+SR and the proposed method can improve the solving speed of the traditional BCM(Blocking Clauses Method)by 4.6 times,13.4 times,7.3 times and 32.4 times,respectively.Compared with BCM,the memory consumption of the proposed scheme is reduced to 35.3%.In addition,the experimental results also show that the performance of this scheme can be further improved through parallelization.

关 键 词：SMT全解求解器 二分查找(BS) 上下文感知(CA) 暂停恢复(SR) 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]