| |||||||
ShanghaiTech University Knowledge Management System
ESAMPLER: Boosting sampling of satisfying assignments for Boolean formulas via derivation | |
2022-08 | |
发表期刊 | JOURNAL OF SYSTEMS ARCHITECTURE (IF:3.7[JCR-2023],3.6[5-Year]) |
ISSN | 1383-7621 |
EISSN | 1873-6165 |
卷号 | 129 |
发表状态 | 已发表 |
DOI | 10.1016/j.sysarc.2022.102615 |
摘要 | Boolean satisfiability (SAT) plays a key role in diverse areas such as spanning planning, inference, data mining, testing and optimization. Apart from the classical problem of checking Boolean satisfiability, generating random satisfying assignments has attracted significant theoretical and practical interests over the past years. In practical applications, usually a large number of satisfying assignments for a given Boolean formula are needed, the generation of which turns out to be a computational hard problem in both theory and practice. In this work, we propose a novel approach to derive a large set of satisfying assignments from a given one in an efficient way. Our approach is based on an insight that flipping the truth values of properly chosen variables of a satisfying assignment could result in satisfying assignments without invoking computationally expensive SAT solving. We propose a derivation algorithm to discover such variables for each given satisfying assignment. Our approach is orthogonal to the previous techniques for generating satisfying assignments and could be integrated into the existing SAT samplers. We implement our approach as an open-source tool ESAMPLER using two representative state-of-the-art samplers (QUICKSAMPLER and UNIGEN3) as the underlying satisfying assignment generation engine. We conduct extensive experiments on various publicly available benchmarks and apply ESAMPLER to solve Bayesian inference. The results show that ESAMPLER can efficiently boost the sampling of satisfying assignments of both QUICKSAMPLER and UNIGEN3 on a large portion of the benchmarks and is at least comparable on the others. ESAMPLER performs considerably better than QUICKSAMPLER and UNIGEN3, as well as another state-of-the-art sampler SearchTreeSampler. © 2022 Elsevier B.V. |
关键词 | Bayesian networks Boolean functions Computational complexity Inference engines Random number generation Boolean formulae Boolean satisfiability Classical problems Constraint-based Constraint-based sampling Data optimization Data testing Satisfiability solving Satisfying assignments State of the art |
URL | 查看原文 |
收录类别 | SCI ; SCIE ; EI |
语种 | 英语 |
资助项目 | National Natural Science Foundation of China (NSFC)[ |
WOS研究方向 | Computer Science |
WOS类目 | Computer Science, Hardware & Architecture ; Computer Science, Software Engineering |
WOS记录号 | WOS:000827328600002 |
出版者 | Elsevier B.V. |
EI入藏号 | 20222612279345 |
EI主题词 | Data mining |
EI分类号 | 721.1 Computer Theory, Includes Formal Logic, Automata Theory, Switching Theory, Programming Theory ; 723.2 Data Processing and Image Processing ; 723.4.1 Expert Systems ; 921.1 Algebra ; 921.4 Combinatorial Mathematics, Includes Graph Theory, Set Theory ; 922.2 Mathematical Statistics |
原始文献类型 | Journal article (JA) |
文献类型 | 期刊论文 |
条目标识符 | https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/200674 |
专题 | 信息科学与技术学院_硕士生 信息科学与技术学院_PI研究组_宋富组 |
通讯作者 | Song, Fu |
作者单位 | 1.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China 2.Univ London, Dept Comp Sci, London, England |
第一作者单位 | 信息科学与技术学院 |
通讯作者单位 | 信息科学与技术学院 |
第一作者的第一单位 | 信息科学与技术学院 |
推荐引用方式 GB/T 7714 | Xu, Yongjie,Song, Fu,Chen, Taolue. ESAMPLER: Boosting sampling of satisfying assignments for Boolean formulas via derivation[J]. JOURNAL OF SYSTEMS ARCHITECTURE,2022,129. |
APA | Xu, Yongjie,Song, Fu,&Chen, Taolue.(2022).ESAMPLER: Boosting sampling of satisfying assignments for Boolean formulas via derivation.JOURNAL OF SYSTEMS ARCHITECTURE,129. |
MLA | Xu, Yongjie,et al."ESAMPLER: Boosting sampling of satisfying assignments for Boolean formulas via derivation".JOURNAL OF SYSTEMS ARCHITECTURE 129(2022). |
条目包含的文件 | ||||||
文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 |
修改评论
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。