Sea una fórmula CNF satisfactoria con n variables y m cláusulas. Sea S F 1 el espacio de solución de F 1 .
Considere el problema de determinar, dado , otra Fórmula CNF F 2 con el mismo conjunto de variables que F 1 , con S F 2 = S F 1 (el mismo espacio de solución que F 1 ), pero con la menor cantidad posible de cláusulas ( el único objetivo es minimizar el número de cláusulas, por lo que cuántos literales puede tener cada cláusula no es relevante).
Pregunta
¿Alguien ya investigó este problema? ¿Hay algún resultado en la literatura al respecto?
Como ejemplo, considere la siguiente Fórmula CNF (cada fila es una cláusula):
x 2 ∨ x 3 ∨ x 4 ¬ x 1 ∨ x 2 ∨ x 4 ¬ x 1 ∨ x 2 ∨ ¬ x 3 ¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2 ∨ ¬ x 5
y la siguiente fórmula :
x 2 ∨ x 3 ∨ x 4 ¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2
ambos tienen el mismo espacio de solución, pero mientras tiene 6 cláusulas, F 2 solo tiene 4 .
Finalmente, considere la siguiente fórmula :
¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2
El espacio de solución es nuevamente el mismo, pero con solo cláusulas.
fuente
Respuestas:
El problema de determinar si existe una fórmula CNF equivalente con un número dado de literales como máximo es -completo. La versión que minimiza el número de cláusulas está dentro de un factor de n del tamaño de la fórmula, donde n es el número de variables. Ver sección 6 de:Πpag2 norte norte
Un resultado reciente muestra que calcular un límite inferior particular para el tamaño de la fórmula CNF equivalente más corta (medida por el número de cláusulas, como usted especifica) es NP-completo. Este documento también afirma que su problema de minimizar el número de cláusulas también es -completo, citando el documento de Umans anterior, aunque por qué esto sigue no me resulta obvio de inmediato.Πpag2
fuente
El problema de minización del circuito es intratable (ver los comentarios a continuación). También creo que puede interesarle la técnica que aplican algunos solucionadores de SAT (al menos hasta cierto punto) que se llama preprocesamiento de SAT. Por ejemplo, el conocido solucionador MiniSAT utiliza un minimizador CNF SatELite para preprocesar una instancia. Google Scholar también ofrece muchos resultados para el "preprocesamiento por satélite".
fuente
La principal solución estándar / conocida para la minimización de CNF en EE es el algoritmo Quine-McCluskey, que tiene muchas implementaciones, algunas de dominio público. Sin embargo, entiendo que (no se menciona en el artículo actual de Wikipedia) la mayoría recurre a algoritmos heurísticos y codiciosos para encontrar soluciones especialmente para fórmulas grandes, es decir, no son necesarias. encuentre la solución óptima esp. para grandes instancias de entrada.
Quine-MCluskey es una generalización del trabajo con mapas de Karnough cuyos diagramas pueden tener éxito en casos pequeños.
y tenga en cuenta que puede haber múltiples soluciones óptimas en términos de fórmulas equivalentes con el mismo tamaño de cláusula (mínimo), esto se señalará en una buena referencia en el subj. encontrar el mínimo aparentemente se reduce a enumerar todas las implicaciones principales que pueden involucrar una explosión exponencial masiva en la memoria / "espacio" en comparación con el tamaño de la fórmula original.
fuente