Clases bien conocidas de fórmulas booleanas que requieren pruebas de resolución exponencialmente largas

27

A menudo puede encontrar métodos de plano de corte, propagación variable, ramificación y encuadernación, aprendizaje de cláusulas, retroceso inteligente o incluso heurística humana tejida a mano en solucionadores SAT. Sin embargo, durante décadas, los mejores solucionadores de SAT se han basado en gran medida en técnicas de prueba de resolución y utilizan una combinación de otras cosas simplemente para obtener ayuda y para dirigir la búsqueda de estilo de resolución. Obviamente, se sospecha que CUALQUIER algoritmo no podrá decidir la pregunta de satisfacción en el tiempo polinómico en al menos algunos casos.

En 1985, Haken demostró en su artículo "La intratabilidad de la resolución" que el principio del palomar codificado en CNF no admite pruebas de resolución de tamaño polinómico. Si bien esto demuestra algo acerca de la intratabilidad de los algoritmos basados ​​en la resolución, también proporciona criterios por los cuales se pueden juzgar los solucionadores de vanguardia, y de hecho, una de las muchas consideraciones que intervienen en el diseño de un solucionador SAT hoy es cómo es probable que funcione en casos "difíciles" conocidos.

Tener una lista de clases de fórmulas booleanas que admitan demostrablemente pruebas de resolución de tamaño exponencial es útil en el sentido de que proporciona fórmulas 'difíciles' para probar nuevos solucionadores SAT. ¿Qué trabajo se ha hecho compilando tales clases juntos? ¿Alguien tiene una referencia que contenga dicha lista y sus pruebas relevantes? Enumere una clase de fórmula booleana por respuesta.

Ross Snider
fuente
wiki de la comunidad?
Opte el
Hice este wiki de la comunidad según la sugerencia.
Ross Snider
1
Un aspecto adicional a esta pregunta que me interesaría: ¿hay pruebas explícitas conocidas de tamaño polivinílico para la resolución extendida para estos casos difíciles (como la prueba de Cook de fórmulas débiles de agujero de paloma)?
MGwynne

Respuestas:

21

Instancias difíciles para la resolución :

  1. Fórmulas de Tseitin (sobre gráficos expansores).

  2. Débil ( a n ) principio del palomar (exponencial de n límites inferiores, para cualquier m > n ).mnnm>n

  3. Random 3CNF de con variables y O ( n 1,5 - ε ) cláusulas, para 0 < ε < 1 / 2 .nO(n1.5ϵ)0<ϵ<1/2

Buena encuesta técnica relativamente actualizada para los límites inferiores de la complejidad de la prueba, ver:

Nathan Segerlind: la complejidad de las pruebas proposicionales. Boletín de Symbolic Logic 13 (4): 417-481 (2007) disponible en: http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Iddo Tzameret
fuente
Este es un buen ejemplo de una respuesta. Sería una respuesta aún mejor si se dividiera en varias.
Ross Snider
9

Hay una serie de buenas encuestas y libros sobre la complejidad de la prueba proposicional que contienen tales listas. Muchos sistemas de prueba simulan resolución, por lo tanto, cualquier fórmula que sea difícil para ellos será difícil de resolver.

Libros:
1. Jan Krajicek, "Aritmética limitada, lógica proposicional y teoría de la complejidad", 1995
2. Stephen A. Cook y Phoung The Neguyen, "Fundamentos lógicos de la complejidad de la prueba", 2010

Encuestas:
1. Paul Beame y Toniann Pitassi, "Complejidad de prueba proposicional: pasado, presente y futuro", 2001
2. Samuel R. Buss, "Complejidad de prueba aritmética y propositiva limitada", 1997
3. Alasdair Urquhart, "La complejidad de pruebas proposicionales ", 1995

También vea los enumerados aquí y aquí .

Kaveh
fuente
8

Otro ejemplo difícil de resolución son las fórmulas de tablero de ajedrez mutiladas. Afirman que un tablero de ajedrez con dos esquinas diagonalmente opuestas que faltan no se puede cubrir con2n×2n2×1

Michael Alekhnovich. El problema del tablero de ajedrez mutilado es exponencialmente difícil de resolver. Theoretical Compututer Science 310 (1-3): 513-525 (2004).http://dx.doi.org/10.1016/S0304-3975(03)00395-5

Jan Johannsen
fuente
8

n(k)22k=12logni,jKxi,ji,jK¬xi,jK{1,,n}|K|=k informe del ECCC .

Jan Johannsen
fuente
Gracias. Esta es una respuesta muy interesante (aunque la notación es un poco diferente, podría seguirla). Mi consejero universitario estudió ampliamente la teoría de Ramsey. Tuvo éxito al instalar ese interés en mí también.
Ross Snider
1

¿ DIMACS no mantiene conjuntos de muestras de instancias de SAT rígidas? No pude encontrarlo allí con solo una mirada superficial, pero si ingresas "SAT" en su cuadro de búsqueda, aparecerán muchos resultados, incluidos varios documentos / charlas sobre instancias de SAT difíciles.

Kurt
fuente
Las instancias difíciles particulares (a diferencia de las familias de instancias) están aquí satcompetition.org (Ver "puntos de referencia".)
Radu GRIGore