Institutional Repository
| Double configuration checking in stochastic local search for satisfiability | |
| Luo, Chuan (1); Cai, Shaowei (2); Wu, Wei (1); Su, Kaile (1); Cai, Shaowei | |
| 2014 | |
| Conference Name | 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 |
| Pages | 2703-2709 |
| Conference Date | July 27, 2014 - July 31, 2014 |
| Conference Place | Quebec City, QC, Canada |
| Indexed Type | EI |
| Publish Place | AI Access Foundation |
| ISBN | 9781577356806 |
| Department | (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 |
| English Abstract | 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. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16609 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Cai, Shaowei |
| Recommended Citation 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. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment