Medir la dificultad de las instancias SAT

28

Dada una instancia de SAT, me gustaría poder estimar lo difícil que será resolver la instancia.

Una forma es ejecutar solucionadores existentes, pero ese tipo de derrota el propósito de estimar la dificultad. Una segunda forma podría ser buscar la relación de cláusulas a variables, como se hace para las transiciones de fase en SAT aleatorio, pero estoy seguro de que existen mejores métodos.

Dada una instancia de SAT, ¿hay algunas heurísticas rápidas para medir la dificultad? La única condición es que estas heurísticas sean más rápidas que la ejecución de solucionadores SAT existentes en la instancia.


Pregunta relacionada

¿Qué problemas de SAT son fáciles? en teoría. Esta pregunta pregunta sobre conjuntos de instancias manejables. Esta es una pregunta similar, pero no exactamente la misma. Estoy realmente interesado en una heurística que, dada una sola instancia, hace una especie de suposición semiinteligente de si la instancia será difícil de resolver.

Artem Kaznatcheev
fuente
¿Puedes explicar por qué la transición de fase wrt "densidad" no es lo que necesitas?
Raphael
@Raphael es un método bastante bueno, y lo menciono en mi pregunta. Pero tuve la impresión de que existen heurísticas aún mejores. La transición de fase que me molesta porque parece muy fácil de engañar (solo agregue cláusulas o instancias fácilmente satisfactorias a la que está tratando de disfrazar)
Artem Kaznatcheev
Lo siento, perdí esa parte de tu pregunta. Correcto, como señalan los comentaristas, la transición de fase parece ser sensible a las fórmulas no aleatorias.
Raphael
2
Puede representar una fórmula SAT (en CNF) como un gráfico bipartito, con vértices para cada fórmula y cláusula y bordes que representan ocurrencias. Si este gráfico es fácil de particionar, entonces el problema puede descomponerse en subgrafos particionados. Tal vez esto puede servir como una medida útil? No tengo idea (por eso es un comentario y no una respuesta).
Alex ten Brink
Puede resultarle útil: ece.uwaterloo.ca/~vganesh/QPaper/paper.pdf
usuario

Respuestas:

22

En general, esta es una pregunta de investigación muy relevante e interesante. "Una forma es ejecutar solucionadores existentes ..." y ¿qué nos diría esto exactamente? Podríamos ver empíricamente que una instancia parece difícil para un solucionador específico o un algoritmo / heurístico específico, pero ¿qué dice realmente sobre la dureza de la instancia?

Una forma que se ha seguido es la identificación de varias propiedades estructurales de instancias que conducen a algoritmos eficientes. De hecho, se prefiere que estas propiedades sean "fácilmente" identificables. Un ejemplo es la topología del gráfico de restricción subyacente, medido utilizando varios parámetros de ancho del gráfico. Por ejemplo, se sabe que una instancia se puede resolver en tiempo polinómico si el ancho del árbol del gráfico de restricción subyacente está limitado por una constante.

Otro enfoque se ha centrado en el papel de la estructura oculta de las instancias. Un ejemplo es el conjunto de puerta trasera , que significa el conjunto de variables de modo que cuando se instancian, el problema restante se simplifica a una clase manejable. Por ejemplo, Williams et al., 2003 [1] muestran que incluso teniendo en cuenta el costo de buscar variables de puerta trasera, uno puede obtener una ventaja computacional general al enfocarse en un conjunto de puerta trasera, siempre que el conjunto sea lo suficientemente pequeño. Además, Dilkina et al., 2007 [2] señalan que un solucionador llamado Satz-Rand es notablemente bueno para encontrar puertas traseras pequeñas y fuertes en una variedad de dominios experimentales.

Más recientemente, Ansotegui et al., 2008 [3] proponen el uso de la complejidad espacial tipo árbol como una medida para los solucionadores basados ​​en DPLL. Demuestran que también el espacio delimitado de forma constante implica la existencia de un algoritmo de decisión de tiempo polinomial, siendo el espacio el grado del polinomio (Teorema 6 en el artículo). Además, muestran que el espacio es más pequeño que el tamaño de los conjuntos de ciclos. De hecho, bajo ciertos supuestos, el espacio también es más pequeño que el tamaño de las puertas traseras.

También formalizan lo que creo que buscas, es decir:

ψΓO(norteψ(Γ))


[1] Williams, Ryan, Carla P. Gomes y Bart Selman. "Puertas traseras a la típica complejidad de los casos". Conferencia conjunta internacional sobre inteligencia artificial. Vol. 18 de 2003.

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

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

Juho
fuente
ψ(Γ)
@ArtemKaznatcheev Creo que el conjunto de puerta trasera es probablemente el único realmente utilizado. Al ejecutar un solucionador, realmente no nos importa la dureza de la fórmula; Sin embargo, la instancia debe ser resuelta. La medición debe darnos una ventaja computacional, o tal vez podamos usarla para elegir una heurística adecuada. Aparte de eso, supongo que las medidas de dureza siguen siendo bastante experimentales.
Juho
1

Dado que conoce la transición de fase, permítame mencionar algunas otras comprobaciones simples que conozco (que probablemente están incluidas en el análisis del gráfico de restricciones):

  • Algunos generadores SAT aleatorios tempranos crearon sin darse cuenta fórmulas en su mayoría fáciles porque usaron "densidad constante", lo que significa una proporción aproximadamente igual de todas las longitudes de las cláusulas. Esto fue en su mayoría fácil porque las unidades y las cláusulas 2 simplifican el problema de manera significativa, como era de esperar, y las cláusulas realmente largas no agregan mucha ramificación o facilitan aún más la hiperresolución. Por lo tanto, parece mejor seguir las cláusulas de longitud fija y variar otros parámetros.
  • El |XEl |El |¬XEl |X
  • v1,v2,v3{v1,v2,...},{v2,v3,...},{v1,v3,...}

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

Hombre cortadora de césped
fuente
0

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

Ercsey-Ravasz y Toroczkai, Optimización de la dureza como caos transitorio en un enfoque analógico para la satisfacción de restricciones , Nature Physics volumen 7, páginas 966–970 (2011).

Este enfoque consiste en reescribir el problema SAT en un sistema dinámico, donde cualquier atractor del sistema es una solución al problema SAT. Las cuencas de atracción del sistema son más fractales a medida que el problema se vuelve más difícil, por lo que la "dificultad" de la instancia SAT puede medirse examinando cuán caóticos son los transitorios antes de que el sistema converja.

En la práctica, esto significa iniciar un grupo de solucionadores desde diferentes posiciones iniciales y examinar la velocidad a la que los solucionadores escapan de los transitorios caóticos antes de llegar a un atractor.

No es difícil encontrar un sistema dinámico para el cual las "soluciones" son soluciones a un problema SAT determinado, pero es un poco más difícil asegurarse de que las soluciones sean todas atrayentes y no repelentes. Su solución es introducir variables de energía (similares a los multiplicadores de Lagrange) para representar cuán gravemente se está violando una restricción e intentar que el sistema minimice la energía del sistema.

Curiosamente, utilizando su sistema dinámico, puede resolver problemas de SAT en tiempo polinómico en una computadora analógica, lo que en sí mismo es un resultado notable. Hay una trampa; Puede requerir voltajes exponencialmente grandes para representar las variables de energía, por lo que desafortunadamente no puede darse cuenta de esto en el hardware físico.

Seudónimo
fuente
1
"utilizando su sistema dinámico, puede resolver problemas de SAT en tiempo polinómico en una computadora analógica, lo que en sí mismo es un resultado notable". No estoy de acuerdo con que esto sea notable. Como notará: requiere precisión exponencial. Este es en realidad un truco estándar que se vincula directamente con la definición de NP. Si pudiera medir exponencialmente precisa, podría intentar estimar el número de rutas de aceptación (o ver como walk dyn sys aleatorio) y ver si es exactamente cero o son pocas (por supuesto, esto requeriría una medición exponencialmente precisa, igual que con el sistema dinámico).
Artem Kaznatcheev
Gracias por eso. No conozco muchos resultados teóricos sobre computación analógica.
Seudónimo el