基于聚类的SAT实例结构分析

摘要

随着信息技术地不断发展和移动互联网时代的到来，信息量出现了爆炸式的增长，如何有效地利用这些数据成为一个非常热门的研究方向。数据挖掘就是从大量数据中分析并找出隐含、有价值的信息的过程。SAT问题（satisfiability problem，简称SAT），即布尔可满足性问题，它是一个逻辑命题，即给定一个命题范式，判断是否存在一组变量的赋值使得该范式为真。
　　近年来，对于SAT问题的研究主要是以局部搜索算法为基础，在算法中加入新的策略。虽然可以在一定程度上改善算法性能，但是对于大型SAT算例，由于子句之间联系的复杂性，使得SAT实例存在潜在的结构性特征，局部搜索算法在求解过程中容易出现相同变元频繁翻转、真子句数量无法改善等问题。所以，可以从SAT实例的角度对SAT问题进行研究，通过数据挖掘技术分析SAT实例中子句与子句之间，变元与子句之间潜在的结构特征。首先，将SAT实例表示成图结构模型，顶点表示SAT实例中的子句，边表示子句与子句之间联系紧密程度；然后采用SAT实例团体结构挖掘算法对SAT实例的图结构模型进行挖掘，找出图结构模型中的团体结构(community structure)；最后，对团体结构进行统计，并计算出团体结构的子句覆盖率和变元覆盖率，分析子句、变元对团体结构的影响大小。
　　实验结果发现，在SAT实例图结构表示中，存在着连通子图，连通子图之间的子句、变元是完全没有关联的，这就将SAT实例分为完全独立的子SAT实例，从而减小算例的复杂性。另一方面在实验中，团体的变元覆盖率在20％左右，子句覆盖率在80%左右，这说明SAT实例团体中，少数的变元覆盖了大部分子句，所以可以通过调整少数变元的赋值，使得团体中大量子句的值为真，为SAT问题求解算法提供新了思路和策略。

目录

封面

声明

中文摘要

英文摘要

目录

1 绪 论*

1.1 研究背景与意义

1.2 国内外研究现状

1.3 本文主要研究内容

1.4 本文组织结构

2 SAT问题及图模型表示

2.1 SAT问题的形式描述

2.2 SAT实例的图模型表示

2.3 SAT实例团体结构挖掘框架

2.4 本章小结

3 SAT实例团体结构分析

3.1 SAT实例团体结构描述

3.2 基于聚类分析的团体结构挖掘

3.3 团体结构对于SAT问题的意义

3.4 本章小结

4 基于K-MEANS的SAT实例团体结构挖掘算法

4.1 k-means算法介绍

4.2 SAT团体结构挖掘算法

4.3 本章小结

5 实验结果和分析

5.1 测试用例

5.2 测试环境与配置

5.3 挖掘算法性能分析

5.4 团体结构实验结果分析

5.5 本章小结

6 总结与展望

6.1 全文总结

6.2 课题展望

致谢

参考文献