Pergunta

Sempre que procuro um algoritmo para 2-Sat, recebo de volta o algoritmo para a forma de decisão do problema:Existe um conjunto legal de valores que satisfaça todas as cláusulas.No entanto, isso não me permite encontrar facilmente um conjunto de valores booleanos satisfatórios.

Como posso encontrar com eficiência um conjunto legal de valores que satisfaça uma instância 2-Sat?

Estou trabalhando em c++ com a biblioteca boost e apreciaria um código que pudesse ser facilmente integrado.

desde já, obrigado

Foi útil?

Solução

Se você tiver um algoritmo de decisão para detectar se existe uma atribuição válida para 2-SAT, poderá usá-lo para realmente descobrir a atribuição real.

Primeiro execute o algoritmo de decisão 2-SAT em toda a expressão.Suponha que diga que há uma atribuição válida.

Agora, se x_1 for literal, atribua x_1 como 0.Agora calcule o 2-SAT para a expressão resultante (você terá que atribuir alguns outros literais por causa disso, por exemplo, se x_1 OR x_3 aparecer, você também precisará definir x_3 como 1).

Se a expressão resultante for 2-Satisfiável, então você pode considerar x_1 como 0, caso contrário, x_1 como 1.

Agora você pode descobrir isso sobre cada literal.

Para um algoritmo mais eficiente, sugiro que você tente usar a abordagem do gráfico de implicação.

Pode encontrar mais informação aqui: http://en.wikipedia.org/wiki/2-satisfiability

A parte relevante:

Uma instância de 2 satisfação é solucionável se e somente se todas as variáveis ​​da instância pertencem a um componente fortemente conectado diferente do gráfico de implicação que a negação da mesma variável.Como os componentes fortemente conectados podem ser encontrados no tempo linear por um algoritmo com base na primeira pesquisa em profundidade, o mesmo limite linear se aplica também à 2 satifiabilidade.

Os literais em cada componente fortemente conectado são todos zero ou todos 1.

Outras dicas

Há pelo menos um algoritmo que lista todas as soluções para um problema de 2-SAT, de Tomas Feder: http://www.springerlink.com/content/j582276p06276l12/

Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow
scroll top