论文摘要
SAT问题是计算机科学和人工智能研究的领域的著名问题。在实际生活中有许多问题可以转化为SAT问题,并通过SAT算法得到很好的解决。故而研究高效的SAT算法是当前重要且具有实际应用价值的研究主题。SAT问题来源非常广泛,由此构成了不同类型的SAT Benchmark。然而同一种SAT算法在不同类型的Benchmark上其效率存在较大的差异,人们普遍认为出现这种现象主要由于内部结构上的差异造成。基于这一考虑,SATzilla将众多的SAT算法整合起来,在求解过程中为不同的类型的Benchmark选择不同的算法,并且取得了成功。从中也可以看出为不同类型的Benchmark设计不同的算法将是解决SAT问题的一个重要的发展趋势之一。本文主要针对结构类似于Model RB模型生成的一类SAT Benchmark设计了一种高效的算法,并将该算法成功地用于解决图着色问题。SAT算法主要分为完备算法和不完备算法两大类。完备算法与不完备性算法不同,它不仅可以保证为可满足SAT问题的给出它的一个模型,同时可以证明不可满足SAT问题的不可满足性,故而大多数SAT算法都是完备性算法。在当前的完备性算法中,大多数都是基于DPLL算法框架设计高效的SAT算法,如zChaff、Rsat等。本文也是基于DPLL框架来设计算法。本文在设计算法时,首先对该类SAT Benchmark的结构进行了分析,将变量进行分组处理,在此基础上将其等价性地转化为分别从各变量分组中选取满足条件的变量的问题,并以DPLL运算框架设计出wRBsat算法。算法使用了向量数组来存储数据,实现算法对数据的高效访问与操作。在设计分支决策时,将决策过程分为两步:首先,分组的选取,并以此实现搜索树的构建;其次,变量的选取,在该步骤中实现搜索路径的选取。该方式使得算法能够更好地选取决策变量,控制搜索树的大小,从而提高算法的效率。算法的运算框架使得在算法中的回溯层次相对较少,历史数据的存储也非常方便,从而使得整个冲突分析和回溯的效率都相对较高。本文对算法进行了测试,实验的结果表明在该类Benchmark上本文所设计的wRBsat算法具有更高效率,同时在本文中对测试的结果进行了分析。此外,本文将图着色问题转化为SAT问题,将该算法成功地用于求解图着色问题。