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

发布时间：2025-01-10 20:57

　　 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%。此外,试验结果表明,可以通过并行化进一步提升方案的性能。

【文章页数】：7 页

【部分图文】：

图1 一个例子阐述二分查找

提出的BS方法和上述方法一样，通过求解φ产生与上述方法相同的第一个模型m0。随后产生6个公式φ1～φ6对应6个任务动态划分搜素空间，如图1所示，如φ6=φ∧((x==50)∧(y==50)∧(z>50))。增量子句来描述子空间边界，如x<50表示子空间：

图2 式（3）的模型数量

图3表明基于BS和BD+CA求解器随着时间增加持续增加内存开销，BCM没有明显增加内存开销，这是由于BCM求解器会变得很慢导致的，如图2所示。图3式（3）的内存消耗

图3 式（3）的内存消耗

图2式（3）的模型数量表1和图3表明，基于BS+CA的求解器比基于BS的求解器需要消耗更多的内存（BS+CA的为4.4倍，BS的为2.2倍）。本文提出的求解器比基于BS+SR的求解器在给定相同内存阈值的情况下暂停恢复需要更多时间，前者41.4，后者8.5。导致这一结果是因为基于....

图4 并行化求解速度提升情况

图4表明本文提出的求解器能够通过并行处理进行加速。两个工作程序能够将平均速度提高到1.62倍，4个工作程序能够将平均速度提高到2.4倍。下一步可以考虑解决以下实现限制提升并发性。所有的工作程序从一个共享的任务队列中获取任务；所有的工作程序添加他们产生的任务到一个共享队列；如果当任....

本文编号：4025433