一种基于DR算法的构造子句预处理策略

作者：刘沛瑶; 宋振明; 张世杰

来源：信息技术, 2019, 43(05): 10-14.

DOI：10.13274/j.cnki.hdzj.2019.05.003

• SAT问题
• DR算法
• 归结算法

DR算法是一种完备的归结算法,但在归结过程中会产生大量的新子句,增加了求解时间,所以提高DR算法效率就成了一个问题。文中提出一种基于DR算法的预处理策略CC(Clauses Conduction),通过缩减子句集的规模,得到一个子子句集,再在其上运行DR算法,使得求解时间减少。这种策略虽不完备,但可以大幅度缩减运行时间。

• 单位
  数学学院; 西南交通大学