La medición de la dificultad de casos SAT

Question

Dada una instancia de SAT, me gustaría ser capaz de estimar lo difícil que será para resolver el caso.

Una forma es ejecutar solucionadores existentes, pero ese tipo de derrotas el propósito de estimar dificultad. Una segunda manera podría estar buscando una la relación de las cláusulas a las variables, como se hace para las transiciones de fase en al azar-SAT, pero estoy seguro existen métodos mejores.

Dada una instancia de SAT, hay algunos heurísticos rápidos para medir la dificultad? La única condición es que estas heurísticas más rápida de lo que realmente ejecuta solucionadores SAT existentes en la instancia.

---

pregunta relacionada

problemas

que estaban sentados son fáciles? en cstheory.SE. Esta pregunta se pregunta acerca de los conjuntos manejables de los casos. Esta es una pregunta similar, pero no exactamente lo mismo. Estoy realmente interesado en una heurística que da un solo ejemplo, hace algún tipo de conjetura semi-inteligente de si la instancia será algo difícil de resolver.

Answer 1

En general, este es un tema de investigación muy relevante e interesante. "Una forma es ejecutar solucionadores existentes ..." y lo que esto incluso decirnos exactamente? Pudimos ver empíricamente que una instancia parece difícil para un disolvente específico o un algoritmo específico / heurística, pero ¿qué es lo que realmente hablar de la dureza de la instancia?

Una manera en que se ha perseguido es la identificación de varias propiedades estructurales de los casos que conducen a algoritmos eficientes. Estas propiedades son de hecho preferían ser "fácilmente" identificable. Un ejemplo es la topología de la gráfica restricción subyacente, medida utilizando diversos parámetros de anchura gráfico. Por ejemplo se sabe que una instancia es resoluble en tiempo polinómico si el treewidth de la gráfica restricción subyacente está limitada por una constante.

Otro enfoque se ha centrado en el papel de estructura oculta de instancias. Un ejemplo es el conjunto de puerta trasera , es decir, el conjunto de variables de tal forma que cuando se crea una instancia, los problemas restantes simplifica a una clase manejable. Por ejemplo, Williams et al., 2003 [1] muestran que incluso cuando se tiene en cuenta el coste de la búsqueda de las variables de puerta trasera, todavía se puede obtener una ventaja computacional general, centrándose en un conjunto de puerta trasera, siempre que el conjunto es suficientemente pequeño. Además, Dilkina et al., 2007 [2] nota que un solucionador de llama Rate-Rand es notablemente bueno en encontrar pequeñas puertas traseras fuertes en una serie de dominios experimentales.

Más recientemente, Ansotegui et al., 2008 [3] proponen el uso del árbol-como espacio de la complejidad como una medida para resolver basadas en DPLL. Demuestran que el espacio también constante acotada implica la existencia de un algoritmo de decisión en tiempo polinomial con ser el espacio el grado del polinomio (Teorema 6 en el papel). Por otra parte, muestran el espacio es menor que el tamaño de ciclo-cutsets. De hecho, bajo ciertos supuestos, el espacio es también menor que el tamaño de puertas traseras.

También formalizar lo que creo que está después, es decir:

Encuentra una medida $ \ psi $, y un algoritmo que da una fórmula $ \ Gamma $ decide satisfacibilidad en el tiempo $ O (n ^ {\ psi (\ Gamma)}) $. Cuanto menor sea la medida es, mejor caracteriza el dureza de una fórmula .

---

[1] Williams, Ryan, Carla P. Gomes, y Bart Selman. "Las puertas traseras a la complejidad caso típico". Conferencia Internacional Conjunta sobre Inteligencia Artificial. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes, y Ashish Sabharwal. "soluciones de compromiso en la complejidad de la detección de puerta trasera". Principios y Práctica de Programación con restricciones (CP 2007), pp. 256-270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy, y Felip Manya. "La medición de la dureza de las instancias del SAT." En Actas de la 23ª Conferencia Nacional sobre Inteligencia Artificial (AAAI'08), pp. 222-228, 2008.

Answer 2

Puesto que usted sabe acerca de la transición de fase, que me permita mencionar algunos otros controles simples que yo sepa (que probablemente se subsume en el análisis gráfico de limitación):

• Algunos generadores SAT aleatorios primeras creadas inadvertidamente fórmulas mayoría fáciles porque utilizaron "densidad constante", lo que significa una proporción aproximadamente igual de todas las longitudes cláusula. Estos eran en su mayoría fácil porque 2-cláusulas y unidades simplifican el problema de manera significativa, como cabe esperar, y realmente cláusulas largos o bien no añaden mucho ramificación o facilitan la hiper-resolución aún mejor. Por lo tanto, parece mejor seguir con las cláusulas de longitud fija y variar otros parámetros.
• Del mismo modo, un poderoso imperio simplificación es pura literal eliminación. Obviamente, una fórmula en realidad es sólo tan fuerte como el número de literales impuros que tiene. Debido a la Resolución crea nuevas cláusulas de numeración $ | x | * | \ lnot x | $ (es decir, el producto de ocurrencias de $ x $ y su negación), el número de resolventes se maximiza cuando hay un número igual de literales positivos y negativos de cada variable. Por lo tanto, equilibrado generadores SAT.
• También hay una técnica llamada "Triángulo Sin SAT", que parece ser bastante fresco [1], que es una especie de generador de fuerza instancia que prohíbe "triángulos". Un triángulo es un conjunto de cláusulas que contienen 3 variables $ v_1, v_2, V_3 $ que se producen por pares en todas las combinaciones en algún conjunto de cláusulas (es decir, $ \ {v 1, v_2, ... \}, \ {v_2, V_3, ... \}, \ {v 1, V_3, ... \} $ ). Aparentemente, triángulos tienden a hacer una fórmula más fácil para solucionadores conocidos.

[1] https://arxiv.org/pdf/1903.03592.pdf

Answer 3

Además de una excelente respuesta de Juho, aquí hay otro enfoque:

Ercsey-Ravasz y Toroczkai, Optimización dureza como el caos transitorio en un enfoque análogo a satisfacción de restricciones , el volumen Nature Physics 7, páginas 966-970 (2011).

Este enfoque es reescribir el problema SAT en un sistema dinámico, donde cualquier atractor de el sistema es una solución al problema del SAT. Las cuencas de atracción del sistema son más fractal como el problema se vuelve más difícil, por lo que la "dificultad" de la instancia de SAT se pueden medir mediante el examen de lo caótico que los transitorios están delante de las converge sistema.

En la práctica, esto significa a partir de un montón de solucionadores de diferentes posiciones iniciales y examinando la velocidad a la que solucionadores escapan los transitorios caóticas antes de llegar a un atractor.

No es difícil llegar a un sistema dinámico para el que las "soluciones" son soluciones a un problema SAT dado, pero es un poco más duro para asegurarse de que las soluciones son todos los atractores y repelentes no. Su solución es introducir las variables de energía (similar a los multiplicadores de Lagrange) para representar lo mal que está siendo violado una restricción, y tratar de conseguir el sistema para minimizar la energía del sistema.

Es interesante el uso de su sistema dinámico, que puede resolver los problemas del SAT en tiempo polinómico en una computadora analógica, que en sí mismo es un resultado notable. Hay una trampa; puede requerir exponencialmente grandes tensiones para representar las variables de energía, por lo que lamentablemente no se puede realizar esto en hardware físico.