带硬约束的MAX—SAT问题又称为Partial MAX—SAT问题，它是SAT问题和MAX—SAT问题的结合，比后两者有着更强的描述问题的能力和更广泛的应用背景。人工智能、电路设计、生物信息学等领域的许多问题都可以转化为Partial MAX—SAT问题。 对含有硬子句和软子句的公式，Partial MAX—SAT问题的目标是要找到一组赋值，在满足所有硬子句的情况下，满足最多的软子句。Partial MAX—SAT问题是NP难的最优化问题，对它的求解算法分为完备算法和非完备算法，当前的研究主要集中在完备算法。 本文首先介绍了MAX—SAT问题的研究现状。然后设计分支定界算法求解Partial MAX—SAT问题。当前的大部分求解器都是给硬子句赋予足够大的权值，把带硬约束的MAX—SAT问题转化为带权值的MAX—SAT问题，而没有利用硬子句的特性。本文在下界计算方面，充分利用硬子句的性质，获得更紧的下界。在推理技术方面，提出适应硬子句的五条推理规则。针对硬子句部分难满足的情况，引进求解SAT问题的子句学习算法。另外还设计了预处理和变量选择策略等技术，从而开发出求解Partial MAX—SAT问题的高效求解器。 本文使用2008年MAX—SAT求解评比的官方数据进行实验。跟当今世界上优秀的求解器作横向的比较，实验结果表明本求解器是具有相当竞争力的。