2-Удовлетворенность и Сильно связанные компоненты
Я знаю, что, применяя сильно связанные компоненты в орграфе, мы можем проверить булеву выполнимость 2-SAT, если задача разрешима за полиномиальное время.
Let's assume the problem is satisfiable.
The question: is there a general algorithm to calculate that solution relying on 2-SAT?
1 ответ
Предполагая, что я правильно понимаю ваш вопрос, да, есть общий алгоритм, чтобы найти решение (то есть удовлетворяющее назначение), используя алгоритм для проблемы выполнимости.
Предположим, что я присваиваю переменной xi значение "true" (чтобы литерал xi был истинным, а ~ xi ложным), чтобы создать новый 2-CNF из оригинала. Если бы мне нужно было выполнить удовлетворение (т. Е. Использовать вещь с SCCs, чтобы найти, удовлетворяет ли новый CNF):
- Что это говорит вам об удовлетворяющих заданиях в исходном CNF, если полученный CNF теперь не выполним?
- Что это говорит вам об удовлетворяющих заданиях в исходном CNF, если полученный CNF все еще выполним?
Идея алгоритма состоит в том, чтобы сделать переменную "ложной", если вы нажмете случай 1, и "истиной", если вы нажмете случай 2, и перебрать каждую переменную (сохраняя присвоения, которые вы сделали для переменных, которые вы уже просматривали), Как только вы сможете ответить на поставленные мной вопросы, вы поймете, что стоит за этим.