Como o algoritmo Tarjan funciona para o 2-SAT
-
28-09-2020 - |
Pergunta
O algoritmo de Tarjan para 2-SAT é baseado na verdade:
uma fórmula 2-CNF é satisfatória se e somente se não houver nenhuma variável que pertença ao mesmo componente fortemente conectado que sua negação.
Mas não encontro nenhuma razão para a direção da direita para a esquerda.como a inexistência de tal variável pode garantir a satisfação da CNF?
Tentei seguir as etapas do algoritmo e fiquei preso aqui:
Para cada componente na ordem topológica reversa, se suas variáveis ainda não tiverem atribuições de verdade, defina todos os literais no componente como verdadeiros.Isso também faz com que todos os literais no componente complementar sejam definidos como falsos.
Não é possível que a variável já esteja atribuída ERRADAMENTE?Quando continuamos atribuindo TRUE por trás, e atribuímos FALSE no meio, mas o TRUE deve ser atribuído à próxima variável.Nesse caso, a viabilidade é interrompida.
É claro que esse tipo de caso nunca acontece porque o algoritmo está certo e muitas pessoas usam bem esse algoritmo.Mas muitos posts dizem isso como coisas triviais.
- Acho que a razão pela qual essas atribuições são possíveis é relevante para a condição simétrica do gráfico, uma vez que (x -> ~x -> y -> ~y) nunca tem atribuições verdadeiras.
Nenhuma solução correta
Outras dicas
uma fórmula 2-CNF é satisfatória se e somente se não houver nenhuma variável que pertença ao mesmo componente fortemente conectado que sua negação.
Mas não encontro nenhuma razão para a direção da direita para a esquerda.como a inexistência de tal variável pode garantir a satisfação da CNF?
Pense em uma atribuição de variável para alguma instância 2-SAT insatisfatória.Isso significa que uma ou mais cláusulas devem permanecer insatisfeitas, qualquer que seja a atribuição.Você altera a configuração de uma ou mais variáveis para satisfazer essas cláusulas, mas isso inevitavelmente deixa alguma nova cláusula ou cláusulas insatisfeitas porque a instância é insatisfatória.A falha da sua alteração em satisfazer a instância implica que o valor de alguma outra variável deve ser alterado.Você repete o procedimento repetidas vezes, alterando outras variáveis conforme a implicação exige, mas nunca consegue satisfazer todas as cláusulas.Eventualmente, porque o número de variáveis é finito, uma falha implica que você altere o valor de uma variável que você já visitou...e essa é a sua implicação circular de $x$ para $bar{x}$ de volta a $x$.Sem uma implicação circular você eventualmente chegará ao fim da cadeia de implicação e terá uma tarefa satisfatória.A única maneira de não chegar ao fim da cadeia é esta ser circular entre uma variável e sua negação.