ограничение программирование сетка сети

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. This ipython notebook демонстрирует кодировку, сравнивая результаты SAT-решения (UNSAT, если есть цикл, SAT в противном случае) с результатами алгоритма поиска в прямом цикле.

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

Переменные:.

у меня есть одна переменных для каждого ребра. Край является «активным» или «использованным», если установлена ​​соответствующая переменная. В моей эталонной реализации ребро имеют индексы 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. Это невозможно для цикла, в котором все узлы в цикле могут быть достигнуты с обеих сторон каждого ребра в цикле.