一次性求解多个SAT问题  

Solution to Set of SAT Problems

作　　者：郑黎辉[1] 左万利[1] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012

出　　处：《吉林大学学报（信息科学版）》2010年第2期136-140,共5页Journal of Jilin University（Information Science Edition）

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

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

关 键 词：自动推理 DPLL算法 可满足性 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]