期刊文献+
任意字段
题名或关键词
题名
关键词
摘要
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到1篇文章
< 1 >
每页显示 20 50 100
已选0条
引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
SharpSMT:a scalable toolkit for measuring solution spaces of SMT(LA)formulas 认领 引用
1
作者 Cunjing GE 《Frontiers of Computer Science》 SCIE EI CSCD 2025年第8期1-8,共8页
In this paper,we present SHARPSMT,a toolkit for measuring solution spaces of SMT(LA)formulas which are Boolean combinations of linear arithmetic constraints,i.e.,#SMT(LA)problems.It integrates SMT satisfiability solvi... In this paper,we present SHARPSMT,a toolkit for measuring solution spaces of SMT(LA)formulas which are Boolean combinations of linear arithmetic constraints,i.e.,#SMT(LA)problems.It integrates SMT satisfiability solving algorithm with various polytope subroutines:volume computation,volume estimation,lattice counting,and approximate lattice counting.We propose a series of new polytope preprocessing techniques which have been implemented in SHARPSMT.Experimental results show that the new polytope preprocessing techniques are very effective,especially on application instances.We believe that SHARPSMT will be useful in a number of areas. 展开更多
关键词 #SMT(LA)problems DPLL(T)algorithm polytope preprocessing techniques volume computation lattice counting
暂未订购 下载PDF
已选0条
引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
在线咨询 使用帮助 返回顶部 意见反馈