2009-11-02 9 views

Respuesta

6

Aquí está la página Wikipedia sobre el tema, que describe un algoritmo de tiempo polinomial. (El algoritmo de fuerza bruta de simplemente probar todas las diferentes asignaciones de verdad es el tiempo exponencial.) Tal vez un poco de explicación adicional ayude.

La expresión "si P luego Q" es solo falsa cuando P es verdadero y Q es falso. Entonces la expresión tiene los mismos valores de la tabla de verdad que "Q or not 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" (el mismo que el otro).

Así que el algoritmo implica reemplazar cada expresión de la forma "A o B", con las dos expresiones, "si no A, luego B" y "si no B, entonces A". (Poniéndolo de otra manera, A y B no pueden ser ambos falsos.)

A continuación, construya un gráfico 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, teniendo cuidado de detectar bucles.

Si una de las variables, A, puede alcanzar "no A", y "no A" también puede llegar a A, entonces la expresión original no es satisfactoria. (Es una paradoja). Si ninguna de las variables hace esto, entonces es satisfactoria.

(no pasa nada si A implica "no A", pero no a la inversa Eso sólo significa que A debe ser negado a satisfacer la expresión..)

42

Si tiene n variables y cláusulas m:

Crea un gráfico con 2n vértices: intuitivamente, cada vértice se asemeja a un literal verdadero o no verdadero para cada variable. Para cada cláusula (a v b), donde a y b son literales, crea un borde de! A a by de! B a a. Estos bordes significan que si a no es verdadero, entonces b debe ser verdadero y vica-versa.

Una vez creado este dírafo, revise el gráfico y vea si hay un ciclo que contiene tanto a como! A para alguna variable a. Si hay, entonces el 2SAT no es satisfactorio (porque a implica! A y vica-versa). De lo contrario, es satisfactorio, y esto incluso puede darte una suposición satisfactoria (elige un literal a para que a no implique! A, forza 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 cuán sensible sea usted a la complejidad de tiempo de su algoritmo.

+3

Este es la mejor explicación que he visto para responder a una pregunta: 2-SAT puede ser verdadero (= solucionable) con la ayuda del dígrafo de implicación. –

0

2 satisfiabilty:!!

si x & x está conectado firmemente luego de x podemos llegar a x de x podemos llegar a x

por lo que en nuestra operación, por si acaso! de x, tenemos solo 2 opciones, 1. Tomando x (x) que conduce a!x x 2.rejecting que conduce a x y tanto las opciones están dando lugar a la paradoja de tomar y rechazar una elección, al mismo tiempo

por lo que el satisfacibilidad es imposible (x!): D

Cuestiones relacionadas