| 一次性求解多个SAT问题 |
| |
| 引用本文： | 郑黎辉,左万利.一次性求解多个SAT问题[J].长春邮电学院学报,2010(2):136-140. |
| |
| 作者姓名： | 郑黎辉 左万利 |
| |
| 作者单位： | 吉林大学计算机科学与技术学院,长春130012 |
| |
| 基金项目： | 基金项目：国家自然科学基金资助项目（60373099）;吉林省科技发展计划基金资助项目（20070533）;国家教育部高等学校博士学科点专项科研基金资助项目（200801830021）;吉林大学基本科研业务费交叉学科与创新基金资助项目（200810025） |
| |
| 摘 要： | 在实际应用中通常需要求解对应CNF（ConjunctiveNormalForm）公式之间仅相差几个子句的一系列SAT（SatisfiabilityProblem）问题，但目前绝大多数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 Changchun Post and Telecommunication Institute,2010(2):136-140. |
| |
| 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 proportional to the size of CNF formulas, close factor and the ratio between the number of clauses and variables. |
| |
| Keywords: | automated reasoning DPLL algorithm satisfiability |
| 本文献已被 维普 等数据库收录！ |
