NP难问题的算法和实验性研究

NP难是计算机科学中的一个重要概念和核心问题，自从它的提出到现在， 人们已经得到了很多重要的理论结果。直观上讲，一个问题一旦被证明是NP难 的就意味着我们很难找到该问题的一个多项式时间的有效算法。但从实用的角 度讲，对于应用中遇到的问题，单单是证明它很难（是NP难的）是不够的，如何 在合理的时间内求解实际问题也是必须解决的现实问题。本文主要侧重于NP难 问题的算法和实验性研究，研究对象主要是可满足性问题、图的顶点染色、图 的子图匹配等NP难问题，以及可满足性模理论的解空间计算和体积估算等扩展 问题。 围绕几个著名的问题，本文的主要工作如下： 针对图染色问题，日本研究人员提出了一种通过组合小图单元得到大的难 实例的方法。他们通过试错的方式手工找到了7个小图单元。我们提出了一种新 的构造算法来系统地生成这类小图单元，用我们的算法生成的难图染色实例， 主流的图染色工具需要指数时间才能求解；在一些专门求解色数比较小的图的 图染色工具上我们的算法生成的实例更难求解。针对皇后图染色问题，我们利 用模型查找工具SEM来对这类问题进行求解，在求解过程中提出了新的变量选 择策略，发现比简单地使用可满足性问题工具和图染色工具效果要好。 针对语义Web推理中的关键问题RDF蕴含关系的判定问题，我们利用从子 图同构问题到可满足性问题的编码方案，把它转化为命题逻辑公式的可满足性 判定问题，并采用了启发式的方法对编码过程进行必要的化简得到较少的布尔 公式，然后再利用高效的可满足性问题工具来求解。这种转化为可满足性问题 的方法，是跟RDF简单蕴含的模型论语义结合比较自然的一个方法。在小规模 实例上，这种方法的效果也很好。 针对布尔和数值混合约束的公式，即可满足性模理论（线性理论）公式的 体积计算这一新问题，我们首先给出一个直接计算体积的方法，然后提出一个 改进的算法，并研究了如何通过引入可满足性模理论中的技术来尝试对该算法 进一步地改进。我们实现了工具并做了实验。在一个实际的程序实例上，我们 还就“热门路径”问题做了实例研究和探讨。 体积计算是一个有广泛应用背景的经典难题（#P难的），但以前的方法要 么只能处理线性约束，要么只具有理论价值（不够实用）；针对含非线性约束的 体积计算问题我们提出了实用的算法，并设计了相应的工具，在低维实例有很 好的逼近效果。