greedy clique decomposition for symbolic satisfiability solving

ISCAS OpenIR

	greedy clique decomposition for symbolic satisfiability solving
	Xu Yanyan; Chen Wei; Su Kaile; Zhang Wenhui
	2012
发表期刊	International Journal of Advancements in Computing Technology
ISSN	2005-8039
卷号	4 期号:10 页码:174-184
摘要	Motivated by the recent theoretical results regarding OBDD proof system, this paper applies a new variable grouping heuristic called greedy clique decomposition to symbolic satisfiability solving. Experimental results are compared against other state-of-the-art satisfiability solving tools, including Ebddres, Minisat, TTS and SSAT. We are able to show that with this new heuristic method, our implementation of an OBDD based satisfiability solver can perform better for certain instances, where conflict graphs possess a clique-like structure.; Motivated by the recent theoretical results regarding OBDD proof system, this paper applies a new variable grouping heuristic called greedy clique decomposition to symbolic satisfiability solving. Experimental results are compared against other state-of-the-art satisfiability solving tools, including Ebddres, Minisat, TTS and SSAT. We are able to show that with this new heuristic method, our implementation of an OBDD based satisfiability solver can perform better for certain instances, where conflict graphs possess a clique-like structure.
收录类别	EI
关键词	Heuristic Methods
部门归属	(1) School of Information Science and Technology Beijing Forestry University China; (2) Naveen Jindal School of Management The University of Texas at Dallas United States; (3) College of Mathematics Physics and Information Engineering Zhejiang Normal University Jinhua China; (4) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15450
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Xu Yanyan,Chen Wei,Su Kaile,et al. greedy clique decomposition for symbolic satisfiability solving[J]. International Journal of Advancements in Computing Technology,2012,4(10):174-184.
APA	Xu Yanyan,Chen Wei,Su Kaile,&Zhang Wenhui.(2012).greedy clique decomposition for symbolic satisfiability solving.International Journal of Advancements in Computing Technology,4(10),174-184.
MLA	Xu Yanyan,et al."greedy clique decomposition for symbolic satisfiability solving".International Journal of Advancements in Computing Technology 4.10(2012):174-184.