No se cree que la satisfacción general (con algunas excepciones, como las cláusulas Horn) tenga una solución algorítmica. Sin embargo, el siguiente algoritmo parece ser una solución para la satisfacción general. ¿Cuál es exactamente la falla con el siguiente algoritmo?
- Sea un conjunto vacío que contendrá todas las variables que necesariamente tienen que ser verdaderas o falsas.
- Sea el conjunto de cláusulas.
- Loop a través de .
- Cada vez que una variable no condicional † se encuentra, sacarlo de e insertarlo en .
- Si esto deja un vacío y la implicación ‡ , eliminar todas las variables en esa implicación vacío de y se insertan en .
- Si esto deja una implicación OR vacía ‡ , cree nuevas instancias del algoritmo, donde cada instancia trate con una variable en la implicación (es decir, si la implicación es: , cree una instancia donde se inserte en , uno donde se inserta en y uno donde e se insertan en ).
- Establezca todas las variables en en el valor que necesariamente tienen que ser.
- Vuelva a insertar las variables en en con sus valores modificados y compruebe si se cumplen todas las cláusulas.
- Si se cumple con la satisfacción, devuelva , de lo contrario devuelva "No satisfecho".
† Una variable no condicional se define como una variable que es necesaria verdadera o falsa, por ejemplo, o .
‡ Una implicación vacía se define como una implicación en la que un lado está vacío (por ejemplo, ) o el otro lado es necesariamente verdadero (por ejemplo, .
Para obtener una comprensión más intuitiva del algoritmo, considere el siguiente conjunto de cláusulas :
El algoritmo hará lo siguiente:
1) Puesto que , , son variables no condicionales, el algoritmo insertarlos en . .
2) Extracción de , y saldrán de las cláusulas vacíos: . Estos se añaden a . .
3) Reinsertar las variables en dará como resultado la violación de las primeras cláusulas: . Como es falso, es falso, lo que significa que se viola la cláusula (v). El algoritmo devolverá "No satisfecho"
Soy consciente de que el algoritmo parece confuso. Por favor, siéntase libre de pedir una aclaración.
De los comentarios ahora me doy cuenta de que no se conoce un algoritmo de satisfacción general eficiente eficiente . Todavía estoy interesado en comentarios sobre mi algoritmo. ¿Funciona? ¿Cómo se compara con los algoritmos comunes?
fuente
Respuestas:
Problema 1
El caso de debería ser una "variable no condicional" con respecto a (es decir, que ahora debería insertarse en ). Si esto no es cierto, entonces su algoritmo necesita un paso adicional para inferir esto. Suponiendo que es una " variable no condicional ", continuamos.(x→y∨y¯¯¯) x x¯¯¯ W (x→y∨y¯¯¯)
Problema 2
NOTA: este es un problema que noté; puede muy bien haber otros problemas.
El problema es que la " implicación OR vacía " se divide en dos algoritmos, es que en su forma actual, la división no cubre todos los casos. En particular:
Comienza con , luego se quita y nos queda con una implicación OR vacía de . Sugiere ahora dividirlo en dos problemas nuevos y resolver cada uno de ellos; uno con y uno donde . Pero esto no cubre todos los casos. ¿Qué pasa con el caso cuando . Sin embargo, su algoritmo nunca considera la posibilidad de que sea falso.(x∨c→y) c (x∨[]→y) x=T∧y=T y=T x=F∨y=F y
Creo que podría solucionarlo formulando los dos nuevos problemas como uno con y otro con .y x¯¯¯
Problema 3
Qué sucede cuando te quedan un montón de cláusulas en el formulario:
o
Después de reducir todo, estas cláusulas permanecerán y no podrá probar su satisfacción fácilmente.
Análisis
Nota : Esta notación "O", , etc., se llama Big O notación . se llama Big-omega.O(something) Ω(something)
Suponiendo que el algoritmo funcionara en general, se ejecutaría en el tiempo del peor caso de , siendo el número de variables. La razón es que cada división del problema en problemas de tamaño similar significa que el algoritmo se ejecuta en tiempo exponencial. Para visualizar este concepto, mire la siguiente imagen de un árbol binario completo (imagen de aquí ):Ω(2m) m
Ahora imagine que el problema original es el nodo en la parte superior. Dividimos el problema en dos problemas en el segundo nivel, pero son de un tamaño similar (solo eliminamos una variable, o de la implicación OR vacía , por lo que todavía tendremos muchas implicaciones OR vacías para hacer cada una nivel). Potencialmente tendremos que dividir el problema veces para deshacernos de las variables . Esto significa que tendremos que lidiar con un árbol con niveles. Un árbol con niveles tiene nodos de hojax y O(m) m m m 2m (nodos en la parte inferior). Esto se llama tiempo exponencial y, de manera informal, está a la par con todos los algoritmos de satisfacción booleana conocidos. Pero también lo es la fuerza bruta: hay posibles asignaciones de las variables, por lo que por la fuerza bruta puede adivinar cada asignación y verificar la satisfacción con un rendimiento similar.2m
fuente
Antes de sentir que tiene un "nuevo" algoritmo SAT, revise el algoritmo de rastreo / búsqueda estándar / clásico en la literatura para el problema que data de ~ 1962, el algoritmo Davis-Putnam-Logemann-Loveland . La mayoría de los algoritmos de retroceso / recursivo para el problema probablemente terminarán pareciéndose a este algoritmo, aunque puede llevar bastante tiempo demostrar esta equivalencia.
Un análisis serio implicaría comparar su algoritmo con ejemplos (o instancias aleatorias) frente a DPLL.
Por lo tanto, es útil simplemente resumir cómo su algoritmo difiere de él. sin revisar su código, las probabilidades son:
Un estudiante universitario inteligente puede entender fácilmente el algoritmo; sin embargo, parece que rara vez se enseña a nivel universitario o en libros de texto universitarios, o tal vez ni siquiera se hace referencia a menudo, lo que puede llevar a una visión o impresión errónea de que los algoritmos SAT básicos no se comprenden bien, etc.
También recientemente me encontré con este sitio "en vivo" llamado ToughSat por Yuen y Bebel por generar instancias difíciles para usar con benchmarking, algunas basadas en factoring [uno de los métodos clásicos de generación de instancias duras de SAT]. hay otros, por ejemplo, DIMAC que almacenan archivos de instancias difíciles aunque puede que ya no esté en línea.
fuente