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

Question

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

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

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

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

Answer 1

Вероятно, не составит труда найти ответ, который вы ожидаете, но вместо этого вот ответ real :

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

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

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

Answer 2

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

Answer 3

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

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])

Получить new литерал для пути path_lit <- get_new_literal() Добавить его в путь: path_clause <- if_then_else(node_lits, path_lit) Перейти к 2, перечислить все пары

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

all_paths <- exactly_one(all_path_clauses)
all_paths <- True

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