图染色(K-Coloring)问题

04 Feb 2020 | C/CPP, SAT-Resolver, Algorithm, graph | | ˚C

代码见https://github.com/jiangzhuti/K-Coloring

问题

判断一个给定的包含n个顶点m条边的无向图能否用k种颜色给顶点染色,要求相邻两顶点颜色不同

分析

这是一个经典的SAT问题。解法是把问题转化成CNF子句,然后使用通用的SAT Resolver即可解决。

K-Coloring 问题包含以下三个约束条件:

  1. 一个顶点必须染某种颜色
  2. 一个顶点最多染一种颜色
  3. 一条边的两个顶点颜色不相同

设二维数组 A[x][y] 代表第x个顶点染成颜色y,值是true/false,那么,上述三个约束条件可以转化成如下的CNF子句:

  1. 一个顶点必须染某种颜色:
      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子句

  2. 一个顶点最多染一种颜色:
      -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子句

  3. 一条边的两个顶点颜色不相同: 设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


Older · View Archive (18)

理解asio中strand的用法

Newer

IRResolver(STL set重叠区间以及异构查询)