| 一次性求解多个SAT问题 |
| |
| 引用本文： | 郑黎辉,左万利. 一次性求解多个SAT问题[J]. 吉林大学学报(信息科学版), 2010, 28(2): 136-140. DOI: 10.3969/j.issn.1671-5896.2010.02.005 |
| |
| 作者姓名： | 郑黎辉 左万利 |
| |
| 作者单位： | 吉林大学,计算机科学与技术学院,长春,130012;吉林大学,计算机科学与技术学院,长春,130012 |
| |
| 基金项目： | 国家自然科学基金资助项目(60373099);;吉林省科技发展计划基金资助项目(20070533);;国家教育部高等学校博士学科点专项科研基金资助项目(200801830021);;吉林大学基本科研业务费交叉学科与创新基金资助项目(200810025) |
| |
| 摘 要： | 在实际应用中通常需要求解对应CNF(Conjunctive Normal Form)公式之间仅相差几个子句的一系列SAT(Satisfiability Problem)问题，但目前绝大多数SAT求解算法都是针对单一SAT问题设计的。为此，基于DPLL提出了nDPLL算法，并在随机问题上对该算法的效率进行测试。实验结果表明，nDPLL算法能一次性求解多个SAT问题，对于特定范围的CNF公式集具有较高的效率，CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大，则nDPLL算法的效率越高。
|
| 关 键 词： | 自动推理 DPLL算法 可满足性 |
Solution to Set of SAT Problems |
| |
| ZHENG Li-hui,ZUO Wan-li. Solution to Set of SAT Problems[J]. Journal of Jilin University:Information Sci Ed, 2010, 28(2): 136-140. DOI: 10.3969/j.issn.1671-5896.2010.02.005 |
| |
| Authors: | ZHENG Li-hui ZUO Wan-li |
| |
| Affiliation: | College of Computer Science and Technology, Jilin University, Changchun 130012,China |
| |
| Abstract: | In practical applications,we always need to resolve a series SAT(Satisfiability Problem) problems which only differ in a few clauses between corresponding CNF(Conjunctive Normal Form) formulas.However,most of current SAT solving algorithms are designed for single SAT problem.An algorithm is proposed which is based on DPLL and can solve a set of SAT problems at a time.Tests on random problems demonstrated that: nDPLL algorithm reflects high efficiency on some CNF formulas;the efficiency of nDPLL is proportio... |
| |
| Keywords: | automated reasoning DPLL algorithm satisfiability |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《吉林大学学报(信息科学版)》浏览原始摘要信息 |
|
点击此处可从《吉林大学学报(信息科学版)》下载全文 |
