基于子句的动态检查强制文字的SAT求解器

• 作者: 常文静 徐扬
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 可满足问题 预处理技术 强制文字 数据结构
• 年，卷（期）: 2019,（2）
• 所属期刊栏目: 人工智能与数据挖掘
• 页码范围: 315-320
• 页数: 6页
• 分类号: TP301.6
• 字数: 4266字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2019.02.018

摘要

检查强制文字是一种重要的预处理方法.结合学习子句, 提出一种在求解过程中使用的策略—基于子句的动态检查强制文字 (CNL), 并且设计了一种易实现低成本的数据结构.分别实现了两个不同版本的求解器:Glucose_PRE和Glucose_CNL, 前者在求解初始时将检查强制文字作为预处理, 后者实现了基于子句的动态检查强制文字策略.实验测试结果表明, 与Glucose_PRE和Glucose3.0求解器相比, 求解器Glucose_CNL在求解2015年和2016年SAT竞赛的应用类型的实例时, 求解实例个数更多, 耗时更少, 说明所提策略和所设计的数据结构均可提高求解器的求解性能.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学系统可信性自动验证国家地方联合工程实验室	186	1462	15.0	32.0
2	常文静	西南交通大学信息科学与技术学院	3	4	1.0	2.0