引入命题逻辑支持组合优化问题的求解——以图顶点染色问题为研究介质

组合优化问题是计算机科学和运筹学的核心问题之一，具有重要的理论价值和广泛的应用背景。组合优化问题在求解过程中往往需要处理大量的逻辑关系。然而，现有求解算法大多只考虑问题的约束条件等表层逻辑关系，未充分挖掘和利用其深层次的内在逻辑关系。本课题拟将组合优化问题的特征与命题逻辑动态结合，借助命题逻辑挖掘和处理问题所蕴涵的内在逻辑关系，并以图顶点染色问题为研究介质，设计高性能的求解算法。研究工作主要包括：实现求解图顶点染色问题的基本算法，该算法在深度优先搜索的同时及时剪枝；实现算法的自学习功能，在求解过程中动态地引入命题逻辑，以便挖掘、表示、简化、利用问题所蕴涵的内在逻辑关系；提高自学习功能的针对性，采用启发式策略设定合理的染色顺序，挖掘导致某染色方案非法的核心原因；归纳引入命题逻辑支持求解组合优化问题的一般原则。本课题有望设计出性能更高的图顶点染色问题求解算法，并推动组合优化问题求解算法的研究。

图顶点染色问题是一个NP完全问题，其完备求解算法的困难就在于随着图的规模的增大，图染色方案数迅速膨胀，以至于在可接受的时间内，人们无法获得一个确定的回答。借助逻辑推理，在对问题解空间的搜索过程中可以大量地剪枝，减少分岔，缩小搜索空间，从而快速地找到问题的解。本项研究的目的就是要借助逻辑推理的方法为图顶点染色问题设计高性能的求解算法。. 图顶点染色问题中包含两种约束关系：一种是显性约束关系，即任何相邻接的两个顶点不能染相同的颜色；另一种是隐性约束关系，即不相邻接的两个顶点之间的约束关系。对于一种基于回溯模式的图顶点染色精确求解算法而言，显性约束能够被直观的发现，回溯算法可容易地利用这种约束关系来减小搜索空间。但是，隐性约束则很难被发现并加以利用。如何挖掘图顶点染色问题中的隐性约束关系，如何描述这种关系并利用这种关系来减小搜索空间、提高问题求解的效率是本课题研究的核心内容。.在本项目的研究工作过程中，我们主要做了两方面的工作，命题逻辑公式可满足性即SAT问题的求解，以图染色问题为研究介质的组合优化问题的求解。所取得的重要研究进展如下：.1. 用命题逻辑的推理方法挖掘图顶点染色问题中的隐性约束关系，并将这种隐性约束描述为CNF范式。.2. 利用SAT子句的单值传播技术，对单子句进行赋值。从而实现对搜索树的剪枝，减小搜索空间。.3. 实现了基于独立集划分以及MAX-SAT推理技术的图顶点染色问题完备求解器。.4. 在设计实现图染色完备求解器的过程中，发现并证明了图顶点染色问题的一个定理。即，一个图与其补图的顶点染色数之乘积不小于该图的顶点数。.5. 在原有的完备算法求解器中嵌入一个近似算法，以进一步提高算法的性能，并以SAT问题为切入点，试图将SAT求解中的先进技术引入至现在的研究工作中。.6. 在SAT问题的试探性研究中，根据最小作用量原理提出了一套新的打分系统PLA Scoring System。