一种基于归结的不完备SAT算法

摘要

很多NP问题都可以转换成SAT问题进行求解,所以关于SAT问题求解算法的研究一直是人工智能的一个重要研究方向.DR算法是一种基于归结的高效算法,但在算法的归结过程中会产生很多的新子句,所以减少新子句的产生提高算法效率的一个途径.本文提出一种策略,在原子句集的子集上进行归结,虽然不完备,但可以大幅度缩短算法的运行时间.