Снижение доступности графов до SAT (CNF)

Вот и я столкнулся с этой проблемой в своем учебнике. Мне было интересно, как свести проблему доступности графа к проблеме SAT (CNF). (т.е. формула выполнима, если существует путь в графе G от начала до конца узла)

1) Я не могу понять, как перейти от того, что можно решить за полиномиальное время (Graph Reachability), к чему-то, что является NP (SAT).

2) Кажется, я не могу найти способ сформулировать эти узлы / ребра Graph в фактические предложения в CNF, которые соответствуют достижимости.

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


graph algorithm sat
person csGeek    schedule 17.06.2019    source источник
comment
cs.stackexchange.com - хорошее место, чтобы спросить, есть ли у вас проблемы с получением ответа здесь, в SO.   -  person ggorlen    schedule 17.06.2019

Ответы (3)


arrow_upward
1
arrow_downward

Вероятно, было бы несложно придумать такой ответ, который вы ожидаете, но вот реальный ответ:

«Сведение» проблемы X к проблеме Y означает преобразование любого экземпляра X в экземпляр Y таким образом, чтобы ответ на Y дает ответ на X. Обычно требуется сокращение P-времени, т. Е. Преобразование задачи и получение ответа должны происходить за полиномиальное время.

Достижимость графа легко решается за линейное время, которое, безусловно, является полиномиальным временем, поэтому сокращение от Graph Reachability до SAT очень просто:

  1. Учитывая проблему достижимости графа, решите ее за линейное время;
  2. Если желаемый путь существует, запишите любой подходящий экземпляр SAT, например (A). В противном случае запишите все неудовлетворительные экземпляры SAT, например (A) & (~ A)
person Matt Timmermans    schedule 17.06.2019

arrow_upward
0
arrow_downward

Несколько лет назад мы делали нечто похожее на вашу задачу. Наш подход был основан именно на алгоритме Флойда-Уоршалла (F.-W.). Интуитивно вам хотелось бы чего-то вроде этого:

  1. Сгенерируйте все возможные пути, используя F.-W. для каждой пары узлов
  2. Создайте предложение, представляющее каждый путь. Это можно описать как «если выбран путь, то должны быть выбраны следующие узлы».
  3. Сгенерируйте предложение, которое объединяет все пути в одну CNF. Скорее всего, это будет пункт «точно_одно».

Чуть формальнее:

  1. Назначьте двоичный литерал каждому узлу в графе. Литерал имеет значение True, если и только если. он принадлежит пути между двумя узлами.
  2. Беги F.-W. для пары узлов
  3. Превратите полученный путь в предложение:
    nodes <- get_nodes_from_path(path)  
    node_lits <- logical_and([n.literal for n in nodes])
  1. Получить новый литерал для пути path_lit <- get_new_literal()
  2. Добавьте его в path a path: path_clause <- if_then_else(node_lits, path_lit)
  3. Перейти к 2, перечислить все пары

Наконец, вы могли сделать следующее:

all_paths <- exactly_one(all_path_clauses)
all_paths <- True

Решатель SAT будет вынужден выбрать один из путей, и это приведет к выбору соответствующих узлов.

person CaptainTrunky    schedule 17.06.2019
comment
Этот ответ, кажется, основан на том, как решить проблему с помощью решателя SAT. Однако я думаю, что автор вопроса искал более общий ответ о том, как уменьшить ДОСТУПНОСТЬ до SAT. - person Jacob Soderlund; 17.06.2019
comment
@JacobSoderlund О, я думаю, ты прав. Тем не менее, это может дать некоторое представление о том, как это сделать. - person CaptainTrunky; 17.06.2019

arrow_upward
0
arrow_downward

Что касается вашего первого вопроса: поскольку вы всего лишь разрабатываете способ уменьшить проблему в P до проблемы в NP (а не наоборот), на самом деле это не проблема. Вы можете превратить любую проблему Graph Reachability в задачу SAT, но это не значит, что вы можете превратить любую проблему SAT в проблему Graph Reachability.

person Jacob Soderlund    schedule 17.06.2019