2-Удовлетворенность и Сильно связанные компоненты

Question

Я знаю, что, применяя сильно связанные компоненты в орграфе, мы можем проверить булеву выполнимость 2-SAT, если задача разрешима за полиномиальное время.

Let's assume the problem is satisfiable.

The question: is there a general algorithm to calculate that solution relying on 2-SAT?

Answer 1

Предполагая, что я правильно понимаю ваш вопрос, да, есть общий алгоритм, чтобы найти решение (то есть удовлетворяющее назначение), используя алгоритм для проблемы выполнимости.

Предположим, что я присваиваю переменной x_i значение "true" (чтобы литерал x_i был истинным, а ~ x_i ложным), чтобы создать новый 2-CNF из оригинала. Если бы мне нужно было выполнить удовлетворение (т. Е. Использовать вещь с SCCs, чтобы найти, удовлетворяет ли новый CNF):

1. Что это говорит вам об удовлетворяющих заданиях в исходном CNF, если полученный CNF теперь не выполним?
2. Что это говорит вам об удовлетворяющих заданиях в исходном CNF, если полученный CNF все еще выполним?

Идея алгоритма состоит в том, чтобы сделать переменную "ложной", если вы нажмете случай 1, и "истиной", если вы нажмете случай 2, и перебрать каждую переменную (сохраняя присвоения, которые вы сделали для переменных, которые вы уже просматривали), Как только вы сможете ответить на поставленные мной вопросы, вы поймете, что стоит за этим.