代码见 https://github.com/jiangzhuti/K-Coloring
问题
判断一个给定的包含 n 个顶点 m 条边的无向图能否用 k 种颜色给顶点染色，要求相邻两顶点颜色不同
分析
这是一个经典的 SAT 问题。解法是把问题转化成 CNF 子句，然后使用通用的 SAT Resolver 即可解决。
K-Coloring 问题包含以下三个约束条件：
- 一个顶点必须染某种颜色
- 一个顶点最多染一种颜色
- 一条边的两个顶点颜色不相同
设二维数组 A[x][y] 代表第 x 个顶点染成颜色y，值是true/false，那么，上述三个约束条件可以转化成如下的 CNF 子句：
- 一个顶点必须染某种颜色:
A[1][1] A[1][2] A[1][3] ..... A[1][k] // 顶点 1 用颜色 1 或 颜色 2 或 颜色 3 ..... 染色 A[2][1] A[2][2] A[2][3] ..... A[2][k] .... ..............................A[n][k]共计 n 条 CNF 子句
- 一个顶点最多染一种颜色:
-A[1][1] -A[1][2] //<=>!(A[1][1] && A[1][2]) 顶点 1 不能同时用颜色 1 和 颜色 2 染色 -A[1][1] -A[1][3] // 顶点 1 不能同时用颜色 1 和 颜色 3 染色 .... //-A[1][2] -A[1][1] <=> -A[1][1] -A[1][2] 省略 -A[1][2] -A[1][3] -A[1][2] -A[1][4] .... -A[n][k-1] -A[n][k]共计
n * k * (k - 1) / 2条 CNF 子句 - 一条边的两个顶点颜色不相同: 设 i、j 是一条边的两个顶点
-A[i][1] -A[j][1] // 顶点 i 和顶点 j 不能同时用颜色 1 染色 -A[i][2] -A[j][2] .... -A[x][k] -A[y][k]共计
m * k条 CNF 子句
解决
随机生成无向图
见ggen.cpp，原理是指定顶点数和成边概率，根据概率随机成边
生成 CNF 子句
见g2cnf.cpp，原理是根据上述分析的三种 CFN 类型，生成 cnf 文件
SAT 求解
采用的通用 SAT 求解器：minisat。该项目现在好像作者不再维护了，修复了几个编译链接选项后，可以编译出可执行文件。比如，使用 ./ggen 20 0.6 g.txt 生成一个包含 20 个顶点、0.6 成边概率的图 g.txt，然后 ./g2cnf g.txt 5 g.cnf 生成 5 种颜色染色的 cnf 文件 g.cnf。然后执行./minisat/build/release/bin/minisat g.cnf g.sat：
$ ./minisat/build/release/bin/minisat g.cnf g.sat
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
| |
| Number of variables: 200 |
| Number of clauses: 2170 |
| Parse time: 0.00 s |
| Eliminated clauses: 0.00 Mb |
| Simplification time: 0.00 s |
| |
============================[ Search Statistics ]==============================
| Conflicts | ORIGINAL | LEARNT | Progress |
| | Vars Clauses Literals | Limit Clauses Lit/Cl | |
===============================================================================
===============================================================================
restarts : 1
conflicts : 0 (0 /sec)
decisions : 92 (0.00 % random) (32822 /sec)
propagations : 180 (64217 /sec)
conflict literals : 0 (-nan % deleted)
Memory used : 10.21 MB
CPU time : 0.002803 s
SATISFIABLE
可以看到显示SATISFIABLE，说明该 SAT 问题可解，并输出结果到 g.sat 中
读取结果
见 sln.cpp。g.sat 内容为上述A[x][y] 每一个元素的真值，通过下标关系即可知道染色方案：
$ ./sln g.cnf g.sat
node 1: color 7
node 2: color 2
node 3: color 4
node 4: color 6
node 5: color 4
node 6: color 5
node 7: color 7
node 8: color 1
node 9: color 6
node 10: color 2
node 11: color 3
node 12: color 10
node 13: color 5
node 14: color 3
node 15: color 5
node 16: color 3
node 17: color 2
node 18: color 1
node 19: color 9
node 20: color 4
正文完