Institutional Repository
| solving difficult sat problems by using obdds and greedy clique decomposition | |
| Xu Yanyan; Chen Wei; Su Kaile; Zhang Wenhui | |
| 2012 | |
| Conference Name | 6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 259-268 |
| Conference Date | May 14, 2012 - May 16, 2012 |
| Conference Place | Beijing, China |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642296994 |
| Department | (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 |
| English Abstract | 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. |
| Keyword | Algorithms Heuristic Methods |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15692 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| 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