solving difficult sat problems by using obdds and greedy clique decomposition

ISCAS OpenIR

	solving difficult sat problems by using obdds and greedy clique decomposition
	Xu Yanyan; Chen Wei; Su Kaile; Zhang Wenhui
	2012
会议名称	6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	259-268
会议日期	May 14, 2012 - May 16, 2012
会议地点	Beijing, China
收录类别	EI
ISSN	0302-9743
ISBN	9783642296994
部门归属	(1) School of Information Science and Technology Beijing Forestry University China; (2) Naveen Jindal School of Management University of Texas Dallas TX United States; (3) College of Mathematics Physics and Information Engineering Zhejiang Normal University Jinhua China; (4) School of Electronics Engineering and Computer Science Peking University China; (5) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China
摘要	In this paper, we propose an OBDD-based algorithm called greedy clique decomposition, which is a new variable grouping heuristic method, to solve difficult SAT problems. We implement our algorithm and compare it with several state-of-art SAT solvers including Minisat, Ebddres and TTS. We show that with this new heuristic method, our implementation of an OBDD-based satisfiability solver can perform better for selected difficult SAT problems, whose conflict graphs possess a clique-like structure. © 2012 Springer-Verlag.; In this paper, we propose an OBDD-based algorithm called greedy clique decomposition, which is a new variable grouping heuristic method, to solve difficult SAT problems. We implement our algorithm and compare it with several state-of-art SAT solvers including Minisat, Ebddres and TTS. We show that with this new heuristic method, our implementation of an OBDD-based satisfiability solver can perform better for selected difficult SAT problems, whose conflict graphs possess a clique-like structure. © 2012 Springer-Verlag.
关键词	Algorithms Heuristic Methods
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15692
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Xu Yanyan,Chen Wei,Su Kaile,et al. solving difficult sat problems by using obdds and greedy clique decomposition[C],2012:259-268.