一次性求解多个SAT问题

作     者：郑黎辉 左万利 ZHENG Li-hui;ZUO Wan-li

作者机构：吉林大学计算机科学与技术学院长春130012 

基　　金：国家自然科学基金资助项目(60373099) 吉林省科技发展计划基金资助项目(20070533) 国家教育部高等学校博士学科点专项科研基金资助项目(200801830021) 吉林大学基本科研业务费交叉学科与创新基金资助项目(200810025) 

出 版 物：《吉林大学学报（信息科学版）》 (Journal of Jilin University（Information Science Edition）)

年 卷 期：2010年第28卷第2期

页      码：136-140页

摘      要：在实际应用中通常需要求解对应CNF(Conjunctive Normal Form)公式之间仅相差几个子句的一系列SAT(Satisfiability Problem)问题,但目前绝大多数SAT求解算法都是针对单一SAT问题设计的。为此,基于DPLL提出了nDPLL算法,并在随机问题上对该算法的效率进行测试。实验结果表明,nDPLL算法能一次性求解多个SAT问题,对于特定范围的CNF公式集具有较高的效率,CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大,则nDPLL算法的效率越高。

主 题 词：自动推理 DPLL算法 可满足性 

学科分类：12[管理学] 1201[管理学-管理科学与工程类] 081104[081104] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1671-5896.2010.02.005

馆 藏 号：203121012...