muse - characteristics of an algorithm
Algoritmo para problema 2-Satisfiabilidad (4)
¿Alguien puede explicar el algoritmo para el problema de 2 satisfacciones o proporcionarme los enlaces para el mismo? No pude encontrar buenos enlaces para entenderlo.
2 satisfacibilidad:
si x &! x está fuertemente conectado entonces desde! x podemos llegar a x desde x podemos llegar a! x
así que en nuestra operación, en el caso de x, solo tenemos 2 opciones, 1.tecir x (x) que conduce a! x 2.el rechazar x (! x) que conduce a x y ambas opciones conducen a la paradoja de Tomando y rechazando una elección al mismo tiempo
por lo que la satisfacibilidad es imposible: D
Aquí está la página de Wikipedia sobre el tema, que describe un algoritmo de tiempo polinomial. (El algoritmo de fuerza bruta de solo probar todas las diferentes asignaciones de verdad es un tiempo exponencial). Tal vez un poco de explicación adicional ayude.
La expresión "si P entonces Q" solo es falsa cuando P es verdadera y Q es falsa. Así que la expresión tiene los mismos valores de tabla de verdad que "Q o no P". También es equivalente a su contrapositivo, "si no es Q entonces no P", y eso a su vez es equivalente a "no P o Q" (lo mismo que el otro).
Así que el algoritmo consiste en reemplazar cada expresión de la forma "A o B", con las dos expresiones, "si no es A, entonces B" y "si no es B, entonces A". (Dicho de otra manera, A y B no pueden ser falsas).
Luego, construye una gráfica que represente estas implicaciones. Cree nodos para cada "A" y "no A", y agregue enlaces para cada una de las implicaciones obtenidas anteriormente.
El último paso es asegurarse de que ninguna de las variables sea equivalente a su propia negación. Es decir, para cada variable A (o no A), siga los enlaces para descubrir todos los nodos a los que se puede acceder desde ella, teniendo cuidado de detectar bucles.
Si una de las variables, A, puede alcanzar "no A", y "no A" también puede alcanzar A, entonces la expresión original no es satisfactoria. (Es una paradoja). Si ninguna de las variables hace esto, entonces es satisfactoria.
(Está bien si A implica "no A", pero no al revés. Eso solo significa que A debe ser negado para satisfacer la expresión).
Se puede resolver con enfoque codicioso. O usando la teoría de grafos, aquí hay un enlace que explica la solución usando la teoría de grafos. http://www.cs.tau.ac.il/~safra/Complexity/2SAT.ppt
Si tienes n variables y cláusulas m:
Cree una gráfica con 2n vértices: intuitivamente, cada vértice se asemeja a un literal verdadero o no verdadero para cada variable. Para cada cláusula (avb), donde a y b son literales, cree un borde de! A a b y de! B a a. Estos bordes significan que si a no es verdadero, entonces b debe ser verdadero y viceversa.
Una vez que se crea este dígrafo, recorra el gráfico y vea si hay un ciclo que contenga tanto a como a para una variable a. Si existe, entonces 2SAT no es satisfactorio (porque a implica! A y vica-versa). De lo contrario, es satisfactorio, y esto puede incluso darte una suposición satisfactoria (elige algún literal a para que no implique! A, fuerza todas las implicaciones desde allí, repítelo). Puede hacer esta parte con cualquiera de sus algoritmos de gráficos estándar, ala Breadth-First Search , Floyd-Warshall , o cualquier algoritmo como estos, dependiendo de lo sensible que esté a la complejidad temporal de su algoritmo.