Если у вас есть алгоритм принятия решения для определения наличия действительного назначения для 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.