Как получить значения 2-Sat
Всякий раз, когда я ищу алгоритм для 2-Sat, я возвращаюсь алгоритм для формы решения проблемы: существует ли допустимый набор значений, который удовлетворяет всем пунктам. Однако это не позволяет мне легко найти набор удовлетворяющих булевых значений.
Как эффективно найти допустимый набор значений, который будет удовлетворять экземпляру 2-Sat?
Я работаю в C++ с библиотекой Boost и был бы признателен за код, который может быть легко интегрирован.
заранее спасибо
2 ответа
Если у вас есть алгоритм принятия решения для определения, существует ли действительное назначение для 2-SAT, вы можете использовать его для фактического определения фактического назначения.
Сначала запустите алгоритм принятия решения 2-SAT для всего выражения. Предположим, он говорит, что есть правильное назначение
Теперь, если x_1 является литералом, присвойте x_1 значение 0. Теперь вычислите 2-SAT для получающегося выражения (из-за этого вам нужно будет назначить некоторые другие литералы, например, если появится x_1 ИЛИ x_3, вам также нужно установить x_3 до 1).
Если полученное выражение является 2-удовлетворяемым, то вы можете взять x_1 равным 0, иначе x_1 к 1.
Теперь вы можете узнать это о каждом литерале.
Для более эффективного алгоритма, я бы посоветовал вам использовать подход графа импликации.
Вы можете найти больше информации здесь: http://en.wikipedia.org/wiki/2-satisfiability
Соответствующая часть:
экземпляр 2-выполнимости разрешим в том и только в том случае, если каждая переменная экземпляра принадлежит другому сильно связному компоненту графа импликации, чем отрицание той же переменной. Поскольку сильно связанные компоненты могут быть найдены в линейное время с помощью алгоритма, основанного на глубинном поиске, такая же линейная временная граница применима также к 2-выполнимости.
Литералы в каждом сильно связанном компоненте либо все ноль, либо все 1.
Там есть по крайней мере один алгоритм, который перечисляет все решения 2-спальной задачи, Томас Федер: http://www.springerlink.com/content/j582276p06276l12/