一次性求解多个SAT问题

• 作者: 左万利 郑黎辉
• 来源期刊: 吉林大学学报(信息科学版)
• 学科: 工学
• 关键词: 自动推理 DPLL算法 可满足性
• 年，卷（期）: 2010,（2）
• 所属期刊栏目: 计算机科学与技术
• 页码范围: 136-140
• 页数: 5页
• 分类号: TP181
• 字数: 3457字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-5896.2010.02.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	左万利	吉林大学计算机科学与技术学院	88	1273	20.0	31.0
2	郑黎辉	吉林大学计算机科学与技术学院	2	1	1.0	1.0