색도에 대한 빠른 정확도 해석기

Question

그래프의 반음계 수를 찾는 것은 NP 하드 문제이므로 '이론적으로는'빠른 솔버가 없습니다. 그래프의 정확한 반음계 수를 신속하게 계산할 수있는 공개적으로 사용 가능한 소프트웨어가 있습니까?

많은 그래프의 반음계를 계산하는 Python 스크립트를 작성하고 있지만 작은 그래프의 경우에도 너무 오래 걸립니다. 그래프 나는 스파 스 또는 밀도가 있지만 일반적으로 10,000 개 미만의 노드 일 수있는 광범위한 그래프로 작업하고 있습니다. 나는 문제를 정수형 프로그램으로 공식화하고 해결하기 위해 구로 비 (Gurobi)에 전달했다. 소프트웨어, 다른 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 솔버를 사용합니다. 나는 그들이 색도가 satsfiability에 가깝다고 생각하기 때문에 정수 프로그램에 대한 감소보다 더 잘 작동 할 것으로 기대한다.

SAT 해결사는 연결 표준 형식에서 명제 부울 수식을 받고 수식이 만족 스러운지 여부를 출력합니다. 다음 문제 COL_k는 NP에 있습니다 :

입력 : 그래프 G와 자연수 k.

출력 : G는 k- 채색이 가능합니다.

COL_k를 해결하려면 꼭지점 u와 색상 1 < = c < = k로 구성된 각 쌍 (u, c)에 대해 하나의 명제 변수가있는 부울 부울 수식으로 인코딩합니다. 모든 정점이 적어도 하나의 색상으로 채색되도록하는 절을 작성해야합니다. 또한 각 모서리가 적절하도록 절이 필요합니다. 그러면 G가 k- 색상이지만 k- (k-1) 색이 아닌 k의 값을 찾기 위해 이진 검색을 수행합니다. 다양한 무료 SAT 해결사가 있습니다. Lingeling을 성공적으로 사용했지만 SAT competition website에서 다른 많은 것을 찾을 수 있습니다. 모두 동일한 입력 및 출력 형식을 사용합니다. Google "MiniSAT 사용자 가이드 : MiniSAT SAT 해 찾기 사용 방법"에서이 형식에 대한 설명을 참조하십시오.

Max-SAT 솔버를 사용할 수도 있습니다. 다시 Max-SAT competition website을 참조하십시오. 그들은 절이 하드 절과 소프트 절로 분할 된 부분 최대 SAT 문제를 해결할 수 있습니다. 여기서 solver는 모든 절을 만족하면서 만족 될 수있는 soft 절의 최대 개수를 찾습니다. Max-SAT competition 웹 사이트 (rules-> details)의 입력 형식을 참조하십시오.

반음계 문제를 하나의 Max-SAT 문제로 공식화 할 수 있습니다 (위와 같은 여러 가지 SAT 문제와 반대). 이런 맥락에서 Max-SAT가 더 적합합니다. 반면 SAT 솔버는 일반적으로 Max-SAT 솔버보다 훨씬 뛰어나다는 인상을 받았습니다. 나는 이런 종류의 솔버에 대한 경험이 없으므로 더 말할 수 없다.