Optimizing Backbone Filtering

doi:10.1109/TASE.2017.8285627

	Optimizing Backbone Filtering
	Zhang, Yueling 3; Li, Jianwen 3; Zhang, Min 1,2,3; Pu, Geguang 3; Song, Fu4
	2017
会议录名称	PROCEEDINGS 11TH 2017 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE)
卷号	2018-January
页码	39-46
发表状态	已发表
DOI	10.1109/TASE.2017.8285627
摘要	Backbone is the common part of each solution in a given propositional formula, which is a key to improving the performance of SAT solving and SAT-based applications, such as model checking and program analysis. In this paper, we propose an optimized approach that combines implication-driven (IDF), conflict-driven (CDF),and unique-driven (UDF) heuristics to improve backbone computing. IDF uses the particular binary structure of the form a <-> b (sic) c to find more backbone literals. CDF comes from the observation that for a clause (sic)a (sic) b, if a is a backbone literal, then b is also a backbone literal. Besides CDF, we are also able to detect new non-backbone literals by UDF. A literal l is not a backbone literal, if there is no clause phi is an element of Phi that is only satisfied by l. We implemented our approach in a tool named DUCIBone with the above optimizations (IDF+CDF+UDF), and conducted experiments on formulas used in previous work and SAT competitions (2015, 2016). Results demonstrate that DUCIBone solved 4% (507 formulas) more formulas than minibones (minibones-RLD, 490 formulas) does under its best configuration. Among 486 formulas solved by all tools (DUCIBone, minibones-RLD, minibonescb-100), DUCIBone reduced 7% (35131 seconds) than minibones (37454 seconds). Experiments indicate that the advantage of DUCIBone is more obvious when the formulas are harder.
关键词	Testing Optimization Computational modeling Filtering Tools Software Integrated circuit modeling
出版地	345 E 47TH ST, NEW YORK, NY 10017 USA
会议地点	Sophia Antipolis
会议日期	13-15 Sept. 2017
URL	查看原文
收录类别	CPCI ; EI
语种	英语
资助项目	MOST NKTSP Project[2015BAG19B02]
WOS研究方向	Computer Science ; Engineering
WOS类目	Computer Science, Software Engineering ; Engineering, Electrical & Electronic
WOS记录号	WOS:000426968400006
出版者	IEEE
EI入藏号	20183105635216
EI主题词	Application programs ; Model checking
EI分类号	Computer Theory, Includes Formal Logic, Automata Theory, Switching Theory, Programming Theory:721.1 ; Computer Software, Data Handling and Applications:723 ; Optimization Techniques:921.5
WOS关键词	COMPUTING BACKBONES ; ALGORITHMS
原始文献类型	Proceedings Paper
来源库	IEEE
引用统计	正在获取...
文献类型	会议论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/18220
专题	信息科学与技术学院_PI研究组_宋富组
通讯作者	Zhang, Min; Pu, Geguang
作者单位	1.East China Normal Univ, MOE Int Joint Lab Trustworthy, Shanghai, Peoples R China 2.East China Normal Univ, Int Res Ctr Trustworthy Software, Shanghai, Peoples R China 3.East China Normal Univ, Comp Sci & Software Engn Inst, Shanghai, Peoples R China 4.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China
推荐引用方式 GB/T 7714	Zhang, Yueling,Li, Jianwen,Zhang, Min,et al. Optimizing Backbone Filtering[C]. 345 E 47TH ST, NEW YORK, NY 10017 USA:IEEE,2017:39-46.