给定一个合取范式CNF,合取范式中的每一项都是布尔变元的析取,SAT问题(Boolean Satisfiability Problem)是判断这个CNF是否可满足;MinSAT问题是指找到一组解使得CNF中满足的子句个数最少,即,使不满足的子句个数最多;MaxSAT问题是指找到一组解使得CNF中满足的子句个数最多,它们都是经典的NP问题。MaxSAT问题和MinSAT问题都是SAT问题的扩展。这些问题在电路控制,社团检测,资源分配选址,AI规划,供应链优化等实际问题中存在着广泛的应用,与最大独立集、最小顶点覆盖、图染色等其它经典的NP难问题的关系也非常密切。研究这些问题具有重要的理论意义和实用价值。本文主要研究SAT问题和MinSAT问题。当前SAT问题和MinSAT问题的求解方法主要分为两种:精确算法和启发式算法。启发式算法通常能很快的给出一个较优解,但无法从理论上保证这个解是全局最优的。精确算法通过搜索问题的整个解空间,从而能确保最终得到的解为全局最优解。从理论上看,现有的NP问题的精确算法在最坏情况下的时间复杂度都是指数级的,但近些年来的研究进步使得精确算法的求解能力得到了显著的提升。本文的研究工作分为两部分,一部分是研究基于DPLL算法的CDCL SAT精确算法,另一部分是研究基于消解规则逻辑推理的MinSAT的理论求解,这两者联系紧密,因为求解SAT问题的精确算法最重要的一点是要尽快找到冲突以减小搜索空间,但是如何更快找到冲突非常不容易。而MinSAT的目标和策略是从子句集中找最多的冲突。我们希望,通过研究MinSAT找最多冲突的策略及这些冲突之间的关系,能对SAT问题的研究带来帮助。本文中的所有研究工作都与冲突的快速寻找密切相关。对于SAT问题,论文从分支启发式,子句库删减和子句化简这三个关键策略展开。具体工作体如下:(一)提出了一个名为nbSAT的策略,用来评估学习子句的质量并根据其进行子句库删减。学习子句对于CDCL SAT求解器的性能至关重要,好的学习子句能引导求解器快速的产生冲突,减小搜索空间。但是,大量学习子句的存在会影响单子句传播的速度,过多的学习子句也会导致内存溢出。为了弥补这些缺点,CDCL SAT求解器的一个常见做法是使用启发式方法评估每个学习子句的质量,并每隔一段时间删除一半低质量的学习子句。提出了nbSAT策略,在SAT求解器Glucose 3.0中做学习子句库删减的时候来评判学习子句的有用性。通过实验研究了nbSAT策略的有效性,并证明它比原始Glucose 3.0中使用的LBD策略更准确。这项改进,再加上一种学习子句消解策略,使得Glucose 3.0在2014年的SAT竞赛的工业算例和人造算例上的表现得到提升。(二)提出了一种基于完整蕴含图的分支启发式策略。好的分支启发式策略能使得求解器快速的找到解或者快速的产生冲突并减小搜索空间。由于现有的分支启发式策略都是基于变元过去参与冲突的情况,除了一些参数不同,在搜索的开始,进行中以及最后,这些分支启发式计算变元分数的方法都是类似的,冲突中所涉及到的所有变元的分数都是增加一个值,而不考虑这些变元对冲突的贡献的区别。然而,在搜索的最开始,一个变元的分数仅仅是基于很少次冲突中其被涉及到的次数,不是非常准确。所以,本文提出了一种分支启发式策略Distance,在搜索的初始化阶段,对完整蕴含图中所涉及的所有变元都根据其到冲突的最长距离打分,而不仅仅只考虑变元的出现次数,从很少的冲突中提取更多的信息,使得能更快的导向冲突的变元分数更高。实验表明,本文提出的分支启发式策略大大提升了求解器的性能,使得求解器在同等时间内能够解决更多的算例。值得一提的是,本文所描述的其中一个使用了Distance分支启发式策略的SAT求解器Maple CM Dist获得了2017年SAT竞赛Main组金牌,而且2018年SAT竞赛Main组的金牌和银牌获得者也都使用了本文提出的Distance策略。(三)将vivification子句化简策略扩展到了对原始子句的化简以及子句二次化简。子句化简策略对搜索过程至关重要,因为短的子句需要更少次的单子句传播就能快速的变成单子句或者产生冲突。本文提出了一种子句选择策略,在预处理过程中和搜索过程中,使用该策略选择一部分原始子句进行化简,并选择部分子句(包括原始子句和学习子句)进行多次化简。更重有的是,本文中做了大量实验对该子句化简策略进行了深入研究分析。结果表明,将本文提出的原始子句化简方法以及子句二次化简策略,可以使得求解器多解决出大量的算例。值得一提的是,本文所描述的其中一个使用了该原始子句化简策略以及子句二次化简策略的SAT求解器获得了2018年SAT竞赛Main组铜牌。对于MinSAT问题:MinSAT问题的目标和策略是找最多的冲突。由于求解SAT问题最重要的一个方向是要尽快找到冲突以使搜索树变得更小。但是如何更快找到冲突非常不容易。众多顶尖高手目前都找不到更好的办法,进展趋于停滞,饱和。而研究MinSAT的目的是通过研究MinSAT找最多冲突的策略及这些冲突之间的关系来寻找如何更快找到冲突的灵感。因此,本文对Bool MinSAT问题也做了一些研究,使用了一种基于消解规则的逻辑推理方式,用于求解MinSAT问题,并对其有效性和完备性做了证明。同时也将该推理规则扩展到多值MinSAT问题上,并也做出来理论证明。根据以上提出的各种改进策略,显著地提高了SAT精确算法求解实际问题的能力。基于以上策略的求解器Maple LCM Dist和Maple CM,分别赢得了2017年SAT竞赛Main组金牌和2018年SAT竞赛Main组铜牌。