组合对象的搜索算法研究

现实世界中的大量问题涉及如何安排有限个离散的基本对象，使之满足特定约束，这类问题可通称为组合问题。本论文主要研究复杂的组合对象的存在性问题。我们特别关注较难求解的组合问题，从算法复杂度上来说，至少是NP难的。由于这些组合对象相应的约束一般都不太容易满足，因此局部搜索等非完备算法方法常常失效。我们致力于研究高效的完备搜索算法，能够在庞大的搜索空间中精准地找到解，当解不存在时，也能够给出确定性的回答。 作者在博士期间的工作可分为两部分：组合数学问题的自动求解和线性约束上的可满足性模理论的体积求解。 我们系统化地研究了组合数学问题的计算机求解，这部分研究包括三大类问题：幂等拟群的大集问题、正交拉丁方和正交数组。这些问题的共同特点是，要寻找的不是一个复杂的组合对象，而是一系列复杂的组合对象，这些对象相互之间还要满足一定的约束。这样一来，搜索空间比寻找单独的一个组合对象要庞大很多倍，问题的难度也大大增加了。对于每一类问题，我们都通过深入研究其结构特征，提出了有效的问题表示方法和搜索方法，发展了一系列新颖的消除同构技术来降低搜索空间，在搜索中我们应用了自动推理最新的技术和工具，如高效的一阶逻辑模型产生器和命题逻辑求解器等，取得了较好的效果。具体来说，我们的工作包括以下三点： (1) n阶幂等拟群的大集问题需要寻找n-2个不相交的幂等拟群，这比寻找单个的满足特定性质的拟群要困难的多。我们设计了约束分割的策略，解决了幂等拟群大集上的一系列开放性问题，特别是得出了LSPQ(11)不存在的结论。我们的方法不但可以回答特定的大集是否存在，还能够确定相互不相交的拟群的最大个数。这些数学结果对朱烈教授等数学家很有意义，并被收入``HandBook of Satisfiability"一书中。 (2) 正交拉丁方的存在性是组合数学中著名的问题。我们利用一阶逻辑有限模型产生器对该问题进行了尝试，提出了一种新的建模方法，称为横截建模，其效果比直接建模方法提高了若干个数量级。同时，我们也提出了一种新的打破对称策略。 (3) 正交数组是一种重要的组合数学结构，可用于软件组件的集成测试。我们设计了一个搜索正交数组的完备性算法，并提出了一些新颖的打破对称技术。与当前的其它工作不同，我们的算法是普适性的，对输入OA参数无任何限制，并且当搜索完成后总能得到确定性的答案。实验表明，我们的工具BOAS在搜索强度为3及其以上的正交数组时非常高效，而用传统的数学方法构造这些数组则很困难，局部搜索算法也对这些数组常常失效。而且，BOAS能够轻易地解决一批对于其它完备算法来说非常难的实例。 我们研究的第二个方面是线性理论上的SMT实例的体积计算问题。关于各类逻辑和约束语言的可满足性问题有大量的研究工作，比如SAT和可满足性模理论（SMT），另一方面，判定问题的计数版本在自动推理中也非常重要。我们研究了SMT的计数版本，即对给定的SMT实例（更精确地说，线性算术约束的布尔组合）如何计算解的个数，或者是说如何计算解空间的体积。这一问题同时扩展了命题逻辑的模型计数问题和凸多面体的体积计算问题。SMT实例的体积计算在许多领域都有潜在的应用价值，比如程序分析与验证和近似推理，但目前还没有相关的研究工作。我们首次研究了这一问题，提出了一个高效的体积计算方法——逐簇法，我们的算法集成了SMT求解中的最新技术。我们的原型工具在随机实例上产生了较好的效果，并可应用在实际的程序实例中，以寻找热门路径。