Быстрые точные решатели для хроматического числа

#graph-algorithm #graph-theory #gurobi #np-hard

#алгоритм графа #теория графов #гуроби #np-жесткий

Вопрос:

Нахождение хроматического числа графика — 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
  

Я ищу способ вычисления точных хроматических чисел, хотя меня бы заинтересовали алгоритмы, которые вычисляют приблизительные хроматические числа, если у них есть разумные теоретические гарантии, такие как приближение с постоянным коэффициентом и т.д.

Ответ №1:

Возможно, вы захотите попробовать использовать SAT-решатель или Max-SAT-решатель. Я ожидаю, что они будут работать лучше, чем сведение к целочисленной программе, поскольку я думаю, что цветопередача ближе к удовлетворяемости.

Решатели SAT получают пропозициональную булеву формулу в конъюнктивной нормальной форме и выводят, является ли формула выполнимой. Следующая проблема COL_k находится в NP:

Входные данные: график G и натуральное число k.

Результат: G может быть k-окрашен.

Чтобы решить COL_k, вы кодируете его как пропозициональную булеву формулу с одной пропозициональной переменной для каждой пары (u, c), состоящей из вершины u и цвета 1<=c<=k. Вам нужно написать предложения, которые гарантируют, что каждая вершина окрашена по крайней мере в один цвет. Вам также нужны предложения, чтобы гарантировать, что каждое ребро правильное. Затем вы просто выполняете двоичный поиск, чтобы найти значение k таким образом, чтобы G было k-раскрашиваемым, но не (k-1)-раскрашиваемым. Существуют различные бесплатные решатели SAT. Я успешно использовал Lingeling, но вы можете найти много других на веб-сайте конкурса SAT. Все они используют один и тот же формат ввода и вывода. Google «Руководство пользователя MiniSat: как использовать решатель MiniSat SAT» для объяснения этого формата.

Вы также можете использовать решатель Max-SAT, снова обратитесь к веб-сайту конкурса Max-SAT. Они могут решить частичную задачу Max-SAT, в которой предложения разбиты на жесткие и мягкие предложения. Здесь решатель находит максимальное количество мягких предложений, которые могут быть выполнены, одновременно удовлетворяя всем жестким предложениям, смотрите формат ввода на веб-сайте конкурса Max-SAT (в разделе правила-> подробности).

Вы можете сформулировать проблему хроматических чисел как одну задачу Max-SAT (в отличие от нескольких задач SAT, как указано выше). В этом смысле Max-SAT подходит лучше. С другой стороны, у меня сложилось впечатление, что решатели SAT обычно работают лучше, чем решатели Max-SAT. У меня нет никакого опыта работы с такого рода решателями, поэтому больше ничего сказать не могу.

Комментарии:

1. Привет, @ tomkot, извините за поздний ответ здесь — я ценю вашу помощь! Я думаю, что решатели SAT — это хороший способ. Однако я обеспокоен тем, что многие из них могут использовать эвристику, такую как WalkSAT, которые застревают в локальных минимумах и возвращают пессимистичные ответы. Я изучу их подробнее и сообщу здесь о том, что я нахожу. Спасибо за вашу помощь! Это определенно была область, о которой я не думал.