Cómo obtener valores 2-Sat
-
22-09-2019 - |
Pregunta
Cada vez que busco un algoritmo para 2-Sat, que vuelva el algoritmo para la forma de decisiones del problema: ¿Existe un conjunto legal de valores que satisfacen todas las cláusulas. Sin embargo, eso no me permite encontrar fácilmente un conjunto de satisfacer valores booleanos.
¿Cómo puedo encontrar de manera eficiente un conjunto legal de valores que va a satisfacer una instancia de 2-Sat?
Estoy trabajando en C ++ con la biblioteca de impulso y agradecería código que puede ser fácilmente integrado.
Gracias de antemano
Solución
Si usted tiene un algoritmo de decisión para detectar si existe una asignación válida para 2-SAT, puede usarlo para encontrar realmente la asignación real.
En primer lugar ejecutar 2-SAT algoritmo de decisión en toda la expresión. Asuma que dice que hay una asignación válida.
Ahora bien, si x_1 es un literal, x_1 Asignar a ser 0. Ahora calculamos el 2-SAT para la expresión resultante (que tendrá que asignar algunos otros literales a causa de esto, por ejemplo si se produce x_1 O x_3, también es necesario a conjunto x_3 a 1).
Si la expresion resultante es 2-satisfiable, entonces puede tomar x_1 a ser 0, de lo contrario toma x 1 a 1.
Ahora usted puede encontrar esto sobre cada literal.
En un algoritmo más eficiente, yo sugeriría que intenta utilizar el enfoque gráfico de implicación.
Puede encontrar más información aquí: http://en.wikipedia.org/wiki/ 2-satisfacibilidad
La parte pertinente:
una instancia de 2-satisfacibilidad es soluble si y sólo si todas las variables de la instancia pertenece a un diferente firmemente conectado componente de la gráfico implicación de la negación de la misma variable. Desde fuertemente componentes conectados se pueden encontrar en tiempo lineal por un algoritmo basado en profundidad primera búsqueda, el mismo lineal de duración limitada se aplica también a 2-satisfacibilidad.
Los literales en cada componente fuertemente conectado o son todos cero o todos 1.
Otros consejos
Hay al menos un algoritmo que enumera todas las soluciones a un 2-sat problema, por Tomas Feder: http://www.springerlink.com/content/j582276p06276l12/