论文标题：SharpSMT: a scalable toolkit for measuring solution spaces of SMT(LA) formulas

期刊：Frontiers of Computer Science

作者：Cunjing GE

发表时间：12 Aug 2024

DOI：10.1007/s11704-024-40500-z

微信链接：点击此处阅读微信文章

引用格式：

Cunjing GE. SharpSMT: a scalable toolkit for measuring solution spaces of SMT(LA) formulas. Front. Comput. Sci., 2025, 19(8): 198336

阅读原文：

问题概述

SharpSMT工具包包含了多种算法，既可以精确求解解空间大小，也可以进行估计。直观上看，SMT(LA)公式的解空间由若干不相交凸多面体构成。因此，总体上工具基于DPLL(T)算法框架枚举凸多面体，并分别对单个凸多面体求解后求和。

技术步骤

工具大致分为4个部分：公式解析与重写、布尔赋值的枚举、凸多面体预处理和凸多面体子过程。文章提出了多种凸多面体的预处理技术并相互结合，如公式分解、变元消除、缓存重用等。

实验结果

大量实验结果表明，基于本文提出的凸多面体预处理技术，可以有效提高计算效率，尤其对于应用问题。

期刊简介

Frontiers of Computer Science （FCS）是由教育部主管、高等教育出版社和北京航空航天大学共同主办，南京大学支持，SpringerNature 公司海外发行的英文学术期刊。本刊于 2007 年创刊，月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为周志华教授，共同主编为熊璋教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐B类期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”；两次入选“中国科技期刊卓越行动计划”（一期梯队、二期领军）。

中国学术前沿期刊网

http://journal.hep.com.cn