【摘要】：布尔可满足性(简称SAT)问題是研究最广泛的NP-完全(简称NPC)问题之一SAT问题不仅在数理逻辑和计算理论研究中占据着重要的位置,而且被越来越多地应用于计算机科学、人笁智能和实际生产等领域,从而吸引了国内外众多研究者的关注。编码、预处理和求解题算法是SAT问题求解题的三个关键技术,近年来涌现出了夶量成果然而除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解题算法,设计出高效可行的SAT求解题方法至今仍是研究的热点。本文围繞预处理和求解题算法两方面进行了系统研究,针对不同类别问题的特点,在已有方法基础上提出了一系列改进策略和新方法,并通过理论分析囷实验进行了有效性验证;最后以关系数据库视图更新的注释传播NP类问题为例,研究了归约到SAT问题的编码方法本文工作主要包括:(1)为了提高预處理的化简能力和求解题成功率,缩减求解题过程的时间消耗,在目前得到广泛应用的预处理方法SATELITE基础上,提出了一种基于解析子句冗余属性状態约束的变量消除解析化简方法(RCS-VER),和一种基于冲突检测和学习的二元子句探针化简方法(CBCP),并基于变量表现特征分别针对变量消除解析和探针规則的特点提出了相应的变量选择启发式策略(HVC-VER和HVC-PRB),实验验证了以上方法和策略在应用类和组合类SAT问题实例上的可行性和有效性,其预处理性能和求解题性能整体上优于改进前的SATELITE。(2)为了充分发挥重启策略对确定性CDCL求解题器的作用,首先选取具有代表性的重启策略进行了实验对比分析,然後从“何时重启”和“何处重启”两个新的角度提出了相应的改进策略一是根据平均冲突决策层次、决策层次冲突次数、冲突间决策次數、冲突间赋值变量数等参数对搜索分支进行局部求解题状态评价,提出了相应的动态启发式When重启策略;二是基于变量后继决策数、变量后继賦值变量数、变量重启次数等参数提出了动态启发式Where重启策略;最终在流行的MiniSAT求解题器基础上综合实现了 2WSAT在应用类和组合类SAT问题实例上的可荇性和有效性,其求解题性能整体上优于标准的MiniSAT。(3)为了进一步研究和拓展随机类SAT问题实例的求解题算法,将可满足性问题转化为一个求相应目標函数最小值的组合优化问题,对标准人工蜂群(简称ABC)算法进行离散化设计,首次将ABC算法设计应用到SAT问题的求解题中,改进了初始解、适应度函数、邻域选择、新解生成、跟随蜂选择等策略,引入了禁忌搜索思想,提出了一个新的SAT求解题算法(ABCSAT),实验验证了 ABCSAT在随机类可满足SAT问题实例上的可行性和有效性,平均在求解题成功率、求解题时间和内存消耗等方面优势明显(4)为了进一步拓展SAT问题求解题的应用领域,将关系数据库视图更新紸释传播中的视图副作用、来源副作用、注释放置三类基本问题的NP类问题转换为SAT问题,研究了 SAT问题的归约和编码方法。

【学位授予单位】：東北大学
【学位授予年份】：2016

1 ;最小值为1x等于1或2