En otro hilo , Joe Fitzsimons preguntó sobre "los mejores límites inferiores actuales en 3SAT".
Me gustaría ir a otro lado: ¿Cuál es el mejor límite superior actual en 3SAT? En otras palabras, ¿cuál es la complejidad temporal del solucionador SAT más eficiente?
En particular, ¿es concebible encontrar un algoritmo sub-exponencial (pero super-polinomial) para SAT?
cc.complexity-theory
ds.algorithms
sat
upper-bounds
MS Dousti
fuente
fuente
Respuestas:
Hay dos tipos de "mejores" solucionadores SAT, uno para teoría y otro para práctica.
Teoría
Práctica
Consulte la conferencia SAT para ver los resultados de la competencia de cada año.
fuente
No conozco ningún algoritmo aleatorio de error cero (o algoritmos coNE / Eadvice ,
para el caso) para SAT que tenga mejores límites que los algoritmos deterministas conocidos,
independientemente de si se promete o no una asignación satisfactoria.
reclama un resultado que se puede resumir de la siguiente manera:
fuente
El algoritmo de Schoening es un algoritmo probabilístico para k-SAT con tiempo de ejecución , donde a = 2 ( k - 1 ) / k . Esto da como resultado un algoritmo O ( 1.33334 n ) para 3SAT, un O ( 1.5 n )O ( anorte) a = 2 ( k - 1 ) / k O ( 1.33334norte) O ( 1.5norte) para 4SAT, etc.
El algoritmo también ha sido (casi completamente) desrandomizado por Moser y Scheder, quienes dan un algoritmo determinista para resolver el tiempo de ejecución de kSAT donde a es la misma constante que antes, y ϵ > 0O((a+ϵ)n) a ϵ>0 se puede hacer arbitrariamente pequeño
Nota: En esta respuesta, la gran notación Oh oculta los factores poli (n). Quería usar la notación , pero no se procesa correctamente.O∗
fuente
Como ya se mencionó, si está interesado en las garantías teóricas de tiempo de ejecución, esta pregunta es un duplicado.
Pero me gustaría señalar que si realmente desea resolver un problema concreto (como el problema de coloración que mencionó), creo que no tiene absolutamente ningún sentido estudiar los límites superiores teóricos.
Aunque deseaba evitar los aspectos de "ingeniería", le sugiero que tome algunos solucionadores SAT populares, los pruebe y vea qué sucede (la mayoría de ellos pueden leer el mismo formato de archivo DIMACS, por lo que es fácil intentarlo diferentes solucionadores). Puede tener sorpresas positivas y negativas. Recientemente tuve una familia de instancias SAT; Un montón de instancias con decenas de miles de variables y más de un millón de cláusulas resultaron fáciles de resolver, mientras que las instancias aparentemente mucho más simples con solo cientos de variables y miles de cláusulas fueron demasiado difíciles para cualquier solucionador que intenté.
fuente
fuente
Es imposible que 3SAT tenga algoritmos sub-exponenciales a menos que la hipótesis del tiempo exponencial sea falsa.
fuente
Esta publicación trata de los límites superiores en SAT. Este uno se ocupa de mejores cotas inferiores. Este enlace brinda detalles de la competencia anual que compara las implementaciones de solucionadores SAT, que se pueden descargar. Para simplificar, puede comenzar con SAT4J , una biblioteca basada en Java para la resolución de SAT.
fuente
El mejor algoritmo determinista para 3-SAT ahora tiene un límite superior 1.32793 ^ n, consulte https://arxiv.org/abs/1804.07901 de Sixue Liu. Básicamente, los límites superiores para todos los k-SAT se han mejorado en este documento.
fuente