Institutional Repository
| greedy clique decomposition for symbolic satisfiability solving | |
| Xu Yanyan; Chen Wei; Su Kaile; Zhang Wenhui | |
| 2012 | |
| Source | International Journal of Advancements in Computing Technology
 |
| ISSN | 2005-8039 |
| Volume | 4Issue:10Pages:174-184 |
| English Abstract | 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. |
| Indexed Type | EI |
| Keyword | Heuristic Methods |
| Department | (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 |
| Language | 英语 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15450 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| 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