クロマの高速完全ソルバ

Question

グラフの色数を見つけることはNP困難な問題であるため、理論的には高速なソルバはありません。グラフの正確な色数をすばやく計算できる一般に公開されているソフトウェアはありますか？

私は、多くのグラフの色数を計算するPythonスクリプトを書いていますが、それは小さなグラフでさえ長すぎます。グラフ私は疎または密であるが通常10,000ノード以下の幅広いグラフを扱っている。私は問題を整数計画として定式化し、それをグロビに渡して解いた。あなたは、ソフトウェア、異なるIP公式、またはこれをスピードアップするための異なるGurobi設定の推奨を持っていますか？私は、彼らがそのような一定の係数近似として合理的な理論的な保証を持っている場合、おおよその色彩の数値を計算するアルゴリズムに興味があるが、正確な色彩の数値を計算するために探しています

import networkx as nx 
from gurobipy import * 

# create test graph 
n = 50 
p = 0.5 
G = nx.erdos_renyi_graph(n, p) 

# compute chromatic number -- ILP solve 
m = Model('chrom_num') 

# get maximum number of variables necessary 
k = max(nx.degree(G).values()) + 1 

# create k binary variables, y_0 ... y_{k-1} to indicate whether color k is used 
y = [] 
for j in range(k): 
    y.append(m.addVar(vtype=GRB.BINARY, name='y_%d' % j, obj=1)) 

# create n * k binary variables, x_{l,j} that is 1 if node l is colored with j 
x = [] 
for l in range(n): 
    x.append([]) 
    for j in range(k): 
     x[-1].append(m.addVar(vtype=GRB.BINARY, name='x_%d_%d' % (l, j), obj=0)) 

# objective function is minimize colors used --> sum of y_0 ... y_{k-1} 
m.setObjective(GRB.MINIMIZE) 
m.update() 

# add constraint -- each node gets exactly one color (sum of colors used is 1) 
for u in range(n): 
    m.addConstr(quicksum(x[u]) == 1, name='NC_%d' % u) 

# add constraint -- keep track of colors used (y_j is set high if any time j is used) 
for u in range(n): 
    for j in range(k): 
     m.addConstr(x[u][j] <= y[j], name='SH_%d_%d' % (u,j)) 

# add constraint -- adjacent nodes have different colors 
for u in range(n): 
    for v in G[u]: 
     if v > u: 
      for j in range(k): 
       m.addConstr(x[u][j] + x[v][j] <= 1, name='ADJ_%d_%d_COL_%d' % (u,v,j)) 

# update model, solve, return the chromatic number 
m.update() 
m.optimize() 
chrom_num = m.objVal 

など

Answer 1

あなたがしようとする場合があります

SATソルバまたはMax-SATソルバを使用する。私は、色度が飽和可能性に近いと考えているので、整数プログラムへの縮小よりもうまくいくと期待しています。

SATソルバーは、Conjunctive Normal Formで命題論理式を受け取り、その式が充足可能かどうかを出力します。次の問題COL_kはNPにある：

入力：グラフGと自然数k。

出力：Gはk-カラー可能です。

COL_kを解決するには、頂点uと色1 < = c < = kからなる各ペア（u、c）に対して1つの命題変数を命題ブール式としてエンコードします。すべての頂点が少なくとも1つの色で色付けされていることを保証する節を書く必要があります。また、各エッジが適切であることを保証するための節が必要です。 次に、バイナリ検索を実行して、Gがk-カラーであるが（k-1）カラーではないようなkの値を見つける。 さまざまなフリーSATソルバーがあります。私はLingelingをうまく使いましたが、多くのものはSAT competition websiteで見つけられます。それらはすべて同じ入力と出力形式を使用します。 Googleの「MiniSATユーザーガイド：MiniSAT SATソルバーの使用方法」を参照してください。

また、Max-SATソルバーを使用することもできます。Max-SAT competition websiteを参照してください。彼らは部分がハード節とソフト節に分割されている部分Max-SAT問題を解決することができます。ここで、ソルバーは、すべてのハード条項を満たしながらも満たすことができるソフト条項の最大数を見つけます（Max-SAT競技ウェブサイトのルール - >詳細の入力形式を参照してください）。

（上記のようないくつかのSAT問題とは対照的に）1つのMax-SAT問題として、有彩色数問題を定式化できます。この意味では、Max-SATはより適しています。一方、SATソルバーは一般にMax-SATソルバーよりも優れたパフォーマンスを発揮するという印象を受けています。私はこのようなソルバの経験がないので、何も言えません。