论文部分内容阅读
人工智能领域中,研究命题逻辑公式的可满足性(SAT)问题具有十分重要的作用。随着科学、技术、社会等领域的发展,需要解决的SAT问题的规模变得越来越大,而传统单一的算法无法适应这些大规模的SAT问题。因此一些针对大规模的SAT问题的求解器应运而生,如Chaff、zChaff、Minisa、Lingeling等诸多著名求解器。这些求解器都并非由单一的算法构建,而是在传统的DPLL等算法的基础上构建的一套系统,如CDCL求解器,其包含多个决策过程,在算法过程中不断的改进学习和调整,以更为高效的解大规模的SAT问题。这些求解器主要分为如下几个部分,分别是变量决策、冲突分析、子句学习和回溯机制。而其中的变量决策过程在整个算法构架中占有十分重要的地位,一个好的变量决策策略可以减少冲突的产生,大量节省求解时间,因此研究变量决策过程的策略具有较为重要的意义。本文主要结合CDCL求解器构架,做了如下几个方面的研究工作：1、本文提出一种启发式策略,根据所给子句、文字数量和出现次数,定义文字相关系数、子句相关系数,进而对初始变量决策过程提供依据；2、基于定义的相关系数,给定冲突状态定义,根据冲突状态下的总的冲突数不断减少的原则,进而定义冲突稳定状态,根据冲突稳定状态制定回溯回退机制策略；3、基于以上两种策略,结合CDCL求解器形成求解SAT问题新算法(Conflict-SAT),并采用SAT竞赛中的问题以及TPTP问题库中旅行商问题进行实例测试,并对测试结果进行分析比较。