标题:Computing and estimating the volume of the solution space of SMT(LA) constraints
作者:Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian
作者机构:[Ge, Cunjing; Ma, Feifei; Zhang, Jian] Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing, Peoples R China.; [Ma, Feifei] Chinese Acad 更多
通讯作者:Ma, Feifei;Ma, FF;Ma, FF;Ma, FF
通讯作者地址:[Ma, FF]Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing, Peoples R China;[Ma, FF]Chinese Acad Sci, Lab Parallel Software & Computat S 更多
来源:THEORETICAL COMPUTER SCIENCE
出版年:2018
卷:743
页码:110-129
DOI:10.1016/j.tcs.2016.10.019
关键词:SMT; Volume; Counting; Convex polytope
摘要:The satisfiability modulo theories (SMT) problem is a decision problem, i.e., deciding the satisfiability of logical formulas with respect to combinations of background theories (like reals, integers, arrays, bit-vectors). In this paper, we study the counting version of SMT with respect to linear arithmetic - SMT(LA), which generalizes both model counting and volume computation of convex polytopes. We describe a method for estimating the volume of convex polytopes based on the Multiphase Monte-Carlo method. It employs a new technique to reutilize random points, so that the number of random points can be significantly reduced. We prove that the reutilization technique has no side-effect on the error. We also investigate a simplified version of hit-and-run method: the coordinate directions method. Based on volume estimation method for polytopes, we present an approach to estimating the volume of the solution space of SMT(LA) formulas. It employs a heuristic strategy to accelerate the volume estimation procedure. In addition, we devise some specific techniques for instances that arise from program analysis. (C) 2016 Elsevier B.V. All rights reserved.
收录类别:EI;SCOPUS;SCIE
WOS核心被引频次:1
Scopus被引频次:1
资源类型:期刊论文
原文链接:https://www.scopus.com/inward/record.uri?eid=2-s2.0-85048737386&doi=10.1016%2fj.tcs.2016.10.019&partnerID=40&md5=abea9507e3028b5bb5982d942e804dcb
TOP