代码见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子句
-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，原理是指定顶点数和成边概率，根据概率随机成边
见g2cnf.cpp，原理是根据上述分析的三种CFN类型，生成cnf文件
采用的通用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