¿Ha habido alguna investigación sobre

25

Una característica bien conocida de las instancias -SAT es la relación del número de cláusulas m sobre el número de variables n , es decir, el cociente ρ = m / n . Para cada k , hay un valor umbral α st \ para ρ α , la mayoría de las instancias son satisfactorias y para ρ α la mayoría de las instancias son insatisfactorias. Se han realizado muchas investigaciones para problemas donde ρ α y para problemas con ρ , k suficientemente pequeñoskmnρ=m/nkαραραραρk-SAT se vuelve solucionable en tiempo polinómico. Ver, por ejemplo, el artículo de la encuesta de Dimitris Achlioptas del Manual de Satisfabilidad ( PDF ).

Me pregunto si se ha realizado algún trabajo en la otra dirección (donde ), por ejemplo, si de alguna manera podemos transformar el problema de CNF a DNF en este caso para resolverlo rápidamente.ρα

Entonces, esencialmente, ¿qué se sabe con respecto al SAT donde ?ρ=m/nα

Matt Groff
fuente
10
Vale la pena señalar que es una función de k . αk
Huck Bennett
¿podría haber alguna transformación que muestre algún tipo de simetría entre las dos regiones en ambos "lados" del punto de transición? Parece plausible. de todos modos, la pregunta es bastante amplia en el sentido de que hay mucho estudio empírico / teórico del punto de transición que no se enfoca tanto en un "lado" u otro ...
vzn

Respuestas:

26

Sí, ha habido Moshe Vardi recientemente dio una charla de encuesta en el taller de Fundamentos teóricos de BIRS sobre la solución de SAT aplicada :

(Moshe presenta la gráfica de su experimento un poco después del minuto 14:30 en su charla vinculada anteriormente).

Deje denotar la relación de la cláusula. A medida que el valor de ρ aumenta más allá del umbral, el problema se vuelve más fácil para los solucionadores de SAT existentes, pero no tan fácil como era antes de alcanzar el umbral. Hay un aumento muy fuerte en la dificultad a medida que nos acercamos al umbral desde abajo. Después del umbral, el problema se vuelve más fácil en comparación con el umbral, pero la disminución de la dificultad es mucho menos pronunciada.ρρ

Supongamos que denota la dificultad del problema wrt a n (en su experimento T ρ ( n ) es la mediana del tiempo de ejecución de GRASP en instancias 3SAT aleatorias con la relación de cláusula ρ ). Moshe sugiere que T ρ ( n ) cambia de la siguiente manera:Tρ(n)nTρ(n)ρTρ(n)

  • el umbral: T ρ ( n ) es polinomial en n ,ρTρ(n)n
  • está cerca del umbral: T ρ ( n ) es exponencial en n ,ρTρ(n)n
  • el umbral: T ρ ( n ) permanece exponencial en n pero el exponente disminuye a medida queaumenta ρ .ρTρ(n)nρ
Kaveh
fuente
1
Cabe señalar que los resultados anteriores son resultados experimentales (de aproximadamente 2000) que utilizan un solucionador SAT específico (GRASP). Pero, teóricamente, se sabe que para una resolución lo suficientemente grande (digamos, Ω ( n ) ) incluso la resolución tiene pequeñas refutaciones de insatisfacción. Y, como Jan Johannsem escribió antes, refutar 3-SAT es fácil (en el caso promedio) ya cuando ρ = Ω ( ρΩ(n). ρ=Ω(n)
Iddo Tzameret
19

k-SAT

  • Para tales fórmulas, se han mostrado límites más bajos en la duración de las refutaciones en la resolución y sistemas de prueba proposicional más fuertes, comenzando con el documento " Muchos ejemplos difíciles para la resolución " de Chvátal y Szemerédi. Estos límites inferiores de resolución implican límites inferiores en el tiempo de ejecución de los solucionadores SAT basados ​​en DPLL y CDCL. Los límites inferiores más fuertes son para el cálculo polinómico, debido a Ben-Sasson e Impagliazzo .
  • Para tales fórmulas, existen algoritmos deterministas eficientes para certificar la insatisfacción, es decir, algoritmos que generan "UNSAT" o "No sé", donde se requiere que la respuesta "UNSAT" sea correcta, y debe generar "UNSAT" en fórmulas insatisfactorias con alta probabilidad. Los mejores resultados en esa dirección se deben a Feige y Ofek .
Jan Johannsen
fuente
km/nc1m/nc2n1/2nc1nc2n3/2
2

Aquí hay un estudio / ángulo más antiguo pero relevante realizado por un experto líder.

κ

κκ

m/nα

vzn
fuente
por otro lado, es presumiblemente posible generar instancias "duras" individuales de cualquier "dimensión" m / n, es solo que son menos probables estadísticamente fuera de la transición de fase "P-NP-P".
vzn