命题逻辑的可满足性问题(SAT)是计算机科学中的核心问题．最大可满足问题(Max-SAT)是SAT问题的一个自然的扩展．对于给定的CNF公式，Max—SAT问题的目标是找到一个赋值使其满足最多的子句．Max-SAT是一个重要的NP-难优化问题．由于人工智能、电路自动设计、统计物理、生物信息学等领域的许多问题都可以转化为Max-SAT问题，所以近十年来，Max-SAT问题引起越来越多的兴趣和关注。 求解Max—SAT的算法可以分为完备算法和不完备算法．就不完备算法而言，Max—SAT和SAT并无很实质的区别，所以当前对Max—SAT算法的研究主要集中在完备算法．设计高效完备算法的关键在于如何进行快速的搜索和有效的推理．本文的工作正集中于这两方面． 在推理方面，本文提出一个比前人更一般的Max-SAT逻辑框架，给出了Ma-—SAT推理中等价、蕴含以及A-等价等概念的形式化定义．在这一基础上，本文进一步给出若干A-等价规则的例子，扩充了求解Max—SAT的推理规则．作为运用推理规贝0的例子，本文利用已有的推理规则改进了前人给出的一个不可满足子句数目的下界． 在搜索方面，当前的完备算法多数采用分支定界的搜索机制．提高分支定界算法效率的关键在于求得紧的下界．本文分析了前人计算下界方法的不足，提出了基于学习的计算方法．具体而言，学习分成两方面．一方面，搜索树中除根结点外的每个结点都向自己的父结点学习不相交的矛盾子句集．另一方面，一种被称之为失败文字检测(failed literal detection，FLD)的方法被之前的一些Max—SAT求解工具用于计算下界；在本文的算法中，搜索树中的每个结点都向过去搜索过的结点学习FLD的有效性，并根据之前的效果来决定在当前结点是否运用FLD．这种基于学习的计算方法，既避免了不必要的计算，又保证了下界的单调性．带权重的Max-SAT问题是MaX—SAT问题的扩展，它们具有更强的描述问题的能力和更广泛的应用．本文将上述方法进一步扩展到带权重的问题，并开发了一系列的求解工具．实验结果表明，这些新的方法，无论是在随机实例还是在由实际问题转换而来的结构化实例，都提高了已有求解工具的性能．值得一提地，其中一个工具LB—SAT在2007年的国际Max-SAT求解评比中，解决了最多的带权实例．而在2008年的Max—SAT求解评比中，我们开发的新求解器IncMaxsatz/IncWMaxsaltz在全部11项评比中，获得3项第一名和4项第二名． 除了设计和实现实用的求解工具以外，本文也从理论上关注Max—SAT算法复杂度的改进．本文定义了和前人不同的非标准复杂性度量，对Max-2-SAT和问题，给出了O*(2K/5.625)的算法，其中K是公式的子句数．用类似的方法，本文还得到Max—CUT问题O*(2M/5.625)的算法，其中M足图中所有边的权重之和．