Ячеистая сеть программирования ограничений

Question

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

E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0поэтому любая из ссылок должна быть неактивной, чтобы не образовывать цикл. Однако в такой сети существует множество возможных петель.

Например петля, образованная ребрами - E0, E3, E7, E11, E15, E12, E5, E1,

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

Может кто-нибудь кинуть какие-нибудь указатели, если есть возможный способ кодировать эту ситуацию? Просто для информации, я использую Z3 Sat Solver.

Answer 1

Следующая кодировка может использоваться с любым графом с N узлы и M кромки. Он использует (N+1)*M переменные и 2*M*M 3-SAT пункты. Этот блокнот ipython демонстрирует кодирование, сравнивая результаты решения SAT (UNSAT, когда есть цикл, SAT в противном случае) с результатами прямого алгоритма поиска цикла.

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

Переменные:

У меня есть одна переменная для каждого края. Ребро "активно" или "используется", если установлена ​​соответствующая переменная. В моей эталонной реализации ребра имеют индексы 0..(M-1) и эти переменные имеют индексы 1..M:

def edge_state_var(edge_idx):
    assert 0 <= edge_idx < M
    return 1 + edge_idx

Тогда у меня есть M переменная состояния ширины бита для каждого ребра, или всего N*M биты состояния (узлы и биты также используют индексацию с нуля):

def node_state_var(node_idx, bit_idx):
    assert 0 <= node_idx < N
    assert 0 <=  bit_idx < M
    return 1 + M + node_idx*M + bit_idx

Статьи:

Когда ребро активно, оно связывает переменные состояния двух узлов, которые соединяет вместе. Биты состояния с тем же индексом, что и у узла, должны быть разными с обеих сторон, а остальные биты состояния должны быть равны их соответствующему партнеру на другом узле. В коде Python:

# which edge connects which nodes
connectivity = [
    ( 0,  1), # edge E0
    ( 1,  2), # edge E1
    ( 2,  3), # edge E2
    ( 0,  4), # edge E3
    ...
]

cnf = list()

for i in range(M):
    eb = edge_state_var(i)
    p, q = connectivity[i]
    for k in range(M):
        pb = node_state_var(p, k)
        qb = node_state_var(q, k)
        if k == i:
            # eb -> (pb != qb)
            cnf.append([-eb, -pb, -qb])
            cnf.append([-eb, +pb, +qb])
        else:
            # eb -> (pb == qb)
            cnf.append([-eb, -pb, +qb])
            cnf.append([-eb, +pb, -qb])

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