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

关键词：可满足问题 预处理技术 强制文字 数据结构 

单位：西南交通大学信息科学与技术学院; 四川成都610036; 西南交通大学系统可信性自动验证国家地方联合工程实验室; 四川成都610036