2-SAT

Um problema de 2-SAT é uma sentença lógica da forma:
(a v b) ^ (~a v c) ^ … (~c v d),
onde a, b, c, d, … são variáveis que você pode atribuir um valor verdade. Dada a sentença, você quer saber se é possível setar valores de forma que a sentença seja verdadeira (e algumas vezes, se sim, quais valores você deve setar para cada variável).

Para isso, a primeira observação é a equivalência lógica entre (a v b) e (~a->b v ~b->a). A partir dela, podemos montar um grafo com vértices representando variáveis e suas negações e colocar uma aresta representando as implicações, como mostra o exemplo abaixo (retirado da wikipedia):

bc3129e2dd11cf8c6848842c23b63921.png

é representado por

300px-Implication_graph.svg.png

Se, para alguma variável, ~x->x e x->~x (onde a implicação pode ser direta ou indireta, ou seja, basta existir um caminho no grafo), a sentença é insatisfatível (a prova disso está no segundo link), ou seja, qualquer combinação de valores das nossas variáveis resultará em falso. Note que essa definição é equivalente a verificar se ~x e x estão na mesma componente conexa, então, após montar o grafo, basta rodar um algoritmo como Kosaraju (descrito no Cormen e aqui) ou Tarjan (que eu uso em ambas as minhas implementações) para separar o grafo em componentes conexas e verificar cada variável com sua negação.

Recuperando o resultado do 2-SAT:

Para recuperar o resultado do 2-SAT, um dos jeitos possíveis é forçar algum valor para as variáveis e rodar o algoritmo de novo. Por exemplo, se queremos ver se a pode ser true, colocamos a aresta ~a->a e rodamos o algoritmo – se o 2-SAT continuar verdadeiro, a=true é uma possível resposta. Essa técnica de recuperação é utilizada na minha solução para o Ministers' Major Mess abaixo e tem complexidade O(n*(n+m))

Links para a teoria:

Problemas envolvendo 2-SAT:

Minha solução: http://pastebin.com/BfRpi1Tw

Minha solução: http://pastebin.com/ebMMrp96

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License