Как работает алгоритм Тарьяна для 2-SAT

Question

Алгоритм Тарьяна для 2-SAT основан на истине:

формула 2-CNF выполнима тогда и только тогда, когда нет переменной, принадлежащей той же сильно связанной составляющей, что и ее отрицание.

Но я не нахожу никаких причин для направления справа налево.как отсутствие такой переменной может гарантировать удовлетворение CNF?

Я попытался следовать шагам алгоритма, и я застрял здесь:

Для каждого компонента в обратном топологическом порядке, если его переменные еще не имеют назначений истинности, задайте всем литералам в компоненте значение true.Это также приводит к тому, что всем литералам в дополнительном компоненте присваивается значение false.

Возможно ли, что переменная уже назначена НЕПРАВИЛЬНО?Когда мы продолжаем присваивать TRUE с обратной стороны и присваиваем FALSE посередине, но TRUE должно быть присвоено следующей переменной.В этом случае нарушается целесообразность.

Конечно, такого рода случаев никогда не бывает, потому что алгоритм правильный, и многие люди хорошо используют этот алгоритм.Но так много постов говорят об этом как о тривиальных вещах.

• Я думаю, что причина, по которой это назначение возможно, имеет отношение к кососимметричному условию графика, поскольку (x -> ~ x -> y -> ~ y) никогда не имеет истинных назначений.

Answer 1

формула 2-CNF выполнима тогда и только тогда, когда нет переменной, принадлежащей той же сильно связанной составляющей, что и ее отрицание.

Но я не нахожу никаких причин для направления справа налево.как отсутствие такой переменной может гарантировать удовлетворение CNF?

Подумайте о присвоении переменной для некоторого неудовлетворительного экземпляра 2-SAT.Это означает, что одно или несколько условий должны оставаться невыполненными независимо от назначения.Вы изменяете настройку одной или нескольких переменных, чтобы они удовлетворяли этим предложениям, но это неизбежно оставляет какое-то новое предложение или предложения неудовлетворенными, поскольку экземпляр является неудовлетворяемым.Неспособность вашего изменения удовлетворить экземпляр подразумевает, что должно измениться значение какой-то другой переменной.Вы повторяете процедуру снова и снова, изменяя другие переменные по мере необходимости, но вам никогда не удается выполнить все условия.В конце концов, поскольку количество переменных ограничено, сбой подразумевает, что вы изменяете значение переменной, которую вы уже посещали...и это ваш круговой вывод из $x$ Для $\бар{x}$ вернуться к $x$.Без круговой импликации вы в конечном итоге достигнете конца цепочки импликаций и получите удовлетворяющее задание.Единственный способ не дойти до конца цепочки - это сделать цепочку замкнутой между переменной и ее отрицанием.