Double configuration checking in stochastic local search for satisfiability

ISCAS OpenIR

	Double configuration checking in stochastic local search for satisfiability
	Luo, Chuan (1); Cai, Shaowei (2); Wu, Wei (1); Su, Kaile (1); Cai, Shaowei
	2014
会议名称	28th AAAI Conference on Artificial Intelligence, AAAI 2014, 26th Innovative Applications of Artificial Intelligence Conference, IAAI 2014 and the 5th Symposium on Educational Advances in Artificial Intelligence, EAAI 2014
页码	2703-2709
会议日期	July 27, 2014 - July 31, 2014
会议地点	Quebec City, QC, Canada
收录类别	EI
出版地	AI Access Foundation
ISBN	9781577356806
部门归属	(1) Key Laboratory of High Confidence Software Technologies, Ministry of Education, Peking University, Beijing, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (3) Queensland Research Laboratory, NICTA, Brisbane, Australia; (4) Australia institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia
摘要	Stochastic local search (SLS) algorithms have shown effectiveness on satisfiable instances of the Boolean satisfiability (SAT) problem. However, their performance is still unsatisfactory on random k-SAT at the phase transition, which is of significance and is one of the empirically hardest distributions of SAT instances. In this paper, we propose a new heuristic called DCCA, which combines two configuration checking (CC) strategies with different definitions of configuration in a novel way. We use the DCCA heuristic to design an efficient SLS solver for SAT dubbed DCCASat. The experiments show that the DCCASat solver significantly outperforms a number of state-of-the-art solvers on ex-tensive random k-SAT benchmarks at the phase transition. Moreover, DCCASat shows good performance on structured benchmarks, and a combination of DCCASat with a complete solver achieves state-of-the-art performance on structured benchmarks.; Stochastic local search (SLS) algorithms have shown effectiveness on satisfiable instances of the Boolean satisfiability (SAT) problem. However, their performance is still unsatisfactory on random k-SAT at the phase transition, which is of significance and is one of the empirically hardest distributions of SAT instances. In this paper, we propose a new heuristic called DCCA, which combines two configuration checking (CC) strategies with different definitions of configuration in a novel way. We use the DCCA heuristic to design an efficient SLS solver for SAT dubbed DCCASat. The experiments show that the DCCASat solver significantly outperforms a number of state-of-the-art solvers on ex-tensive random k-SAT benchmarks at the phase transition. Moreover, DCCASat shows good performance on structured benchmarks, and a combination of DCCASat with a complete solver achieves state-of-the-art performance on structured benchmarks.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16609
专题	中国科学院软件研究所
通讯作者	Cai, Shaowei
推荐引用方式 GB/T 7714	Luo, Chuan ,Cai, Shaowei ,Wu, Wei ,et al. Double configuration checking in stochastic local search for satisfiability[C]. AI Access Foundation,2014:2703-2709.