¿Explicaciones teóricas para el éxito práctico de los solucionadores de SAT?

43

¿Qué explicaciones teóricas existen para el éxito práctico de los solucionadores de SAT, y alguien puede dar una descripción y explicación "estilo wikipedia" uniéndolos a todos?

Por analogía, el análisis suavizado ( versión arXiv ) para el algoritmo simplex hace un gran trabajo explicando por qué funciona tan bien en la práctica, a pesar de que lleva un tiempo exponencial en el peor de los casos y es NP-mighty ( versión arXiv ).

He escuchado un poco sobre cosas como las puertas traseras, la estructura del gráfico de la cláusula y las transiciones de fase, pero (1) no veo cómo encajan todas para dar una imagen más amplia (si es que lo hacen) y (2) No sé si esto realmente explica por qué los solucionadores SAT funcionan tan bien, por ejemplo, en instancias industriales. Además, cuando se trata de cosas como la estructura del gráfico de cláusula: ¿por qué los solucionadores actuales pueden aprovechar ciertas estructuras de gráfico de cláusula?

Solo encuentro los resultados sobre las transiciones de fase parcialmente satisfactorios a este respecto, al menos en mi comprensión actualmente limitada. La literatura de transición de fase trata sobre instancias de k-SAT aleatorio , pero ¿eso realmente explica algo sobre instancias del mundo real? No espero que las instancias de SAT del mundo real se vean como instancias aleatorias; ¿debería? ¿Hay alguna razón para pensar que las transiciones de fase nos dicen algo, incluso intuitivamente, sobre instancias del mundo real, incluso si no parecen instancias aleatorias?

Preguntas relacionadas que ayudan, pero no responden completamente a mi pregunta, en particular la solicitud de vincular las cosas en una imagen coherente:

Joshua Grochow
fuente
55
Esta no es una respuesta, pero no creo que mucha gente todavía crea que las estructuras gráficas / puertas traseras pueden explicar el rendimiento de los solucionadores de SAT. Parecen más relevantes para problemas más difíciles como #SAT, QBF o la recopilación de conocimientos, donde realmente necesita encontrar factorizaciones inteligentes, ya que tiene que explorar de alguna manera toda la estructura. Para su pregunta, me siento tentado a responder "nadie lo sabe realmente y esta es un área activa de investigación". Pero necesito reunir referencias para mostrar lo que la gente está intentando y puede haber alguien con una visión más amplia que yo que pueda dar una mejor respuesta.
holf
2
@Joshua: El método simplex es incluso poderoso para PSPACE (Fearnley y Savani, STOC 15).
Rahul Savani
1
Estoy de acuerdo con @holf. He aquí mi pocos centavos: solucionadores SAT puede recuperarse más rápido que solucionadores de CSP porque todas sus variables tienen un tamaño de dominio de dos. Esto no quiere decir que ningún solucionador de CSP pueda vencer a un solucionador de SAT, puede hacerlo si tiene una heurística de ordenamiento de variables dinámicas (así como un valor) muy sofisticada junto con una buena codificación del problema. Además, cuando convierte una "instancia de la vida real" en una instancia de SAT, rara vez termina en el punto de transición de fase debido a la introducción de tantas variables auxiliares. usually
Tayfun Pay
3
@TayfunPay: No cuestionaba su experiencia; de hecho, creo que 100% los problemas de la "vida real" se traducen en instancias de SAT que no están cerca de la transición de fase. Pero no creo que eso explique la facilidad de tales instancias, ya que esas instancias no son aleatorias , por lo que la transición de fase (en teoría) debería tener poco que decir sobre ellas (dureza o facilidad).
Joshua Grochow
2
Esto ya se ha mencionado en otra parte, pero es importante tener en cuenta que la densidad de cláusula variable y las transiciones de fase son relevantes solo para k-SAT aleatorio y no tiene nada que ver con la dureza de las instancias provenientes de problemas industriales o combinatorios. Por lo tanto, la mayor parte de la discusión anterior no viene al caso. Además, vale la pena señalar que con respecto al k-SAT aleatorio no hay un patrón real fácil-difícil-fácil --- para los sistemas de prueba donde tenemos límites inferiores para fórmulas k-CNF generadas aleatoriamente, las fórmulas permanecen exponencialmente duras para constantes arbitrariamente grandes densidades por encima del umbral.
Jakob Nordstrom

Respuestas:

21

Supongo que se está refiriendo a los solucionadores CDCL SAT en conjuntos de datos de referencia como los utilizados en la Competencia SAT . Estos programas se basan en muchas heurísticas y mucha optimización. Hubo algunas presentaciones muy buenas sobre cómo funcionan en el taller de Fundamentos teóricos de la solución SAT aplicada en Banff en 2014 ( videos ).

Estos algoritmos se basan en el algoritmo de retroceso DPLL que intenta encontrar una asignación satisfactoria estableciendo valores en variables y retrocesos cuando encuentra un conflicto. La gente ha visto cuánto impacto tienen estas heurísticas. Ej. Ver

Parece que la eficiencia de estos solucionadores SAT en los puntos de referencia proviene principalmente de dos dos heurísticas (y sus variantes):

  1. Abeto heurístico VSIDS seleccionando en qué variable ramificarse a continuación.
  2. CDCL: cláusula basada en conflictos de aprendizaje heurístico que aprende una nueva cláusula de un conflicto.

Es bien sabido que las pruebas DPLL corresponden a pruebas en resolución. Sin CDCL, las únicas pruebas de resolución que podemos obtener son pruebas de resolución de árbol que son mucho más débiles que las pruebas de resolución general.

Hay resultados que muestran con CDCL que podemos obtener cualquier prueba de resolución general. Sin embargo, hay advertencias, necesitan muchos reinicios artificiales, ramificaciones artificiales y / o preprocesamiento particular, por lo que no está claro qué tan cerca están de lo que hacen estos programas en la práctica. Consulte, por ejemplo, el siguiente documento para obtener más detalles:


CDCL es esencialmente cortar ramas del espacio de búsqueda. Hay varias formas de derivar una nueva cláusula aprendida de un conflicto. Idealmente, agregaríamos un conjunto de cláusulas mínimas que implicaran el conflicto, pero en la práctica eso puede ser grande y costoso de calcular. Los principales solucionadores de SAT a menudo eliminan cláusulas aprendidas regularmente y eso ayuda en la práctica.


El otro VSIDS heurístico esencialmente mantiene una puntuación para cada variable. Cada vez que hay un conflicto, todos los puntajes se ajustan multiplicándolos con un valor <1 y agregando una constante a los que estuvieron "involucrados" en el conflicto. Para ver lo que esto significa, piense en la secuencia F ( v , i ) que es 1 si la variable v estuvo "involucrada" en el i- ésimo conflicto. Deje que 0 < α < 1 sea ​​una constante fija. El puntaje de la variable v en el tiempo n es entonces: i < n F ( v , i )αF(v,i)i0<α<1vn

i<nF(v,i)α(ni)

Intuitivamente, se puede decir que esto intenta enfatizar variables que estuvieron involucradas consistentemente en conflictos recientes. También puede considerarlo como una forma simplista pero extremadamente barata de predecir qué variables estarán involucradas en el próximo conflicto. Entonces VSIDS se ramifica primero en esas variables. Se puede afirmar que el algoritmo es esencialmente un algoritmo de falla rápida, encuentra conflictos rápidamente. Rápido está relacionado con un menor número de variables establecidas, lo que significa bloquear grandes subárboles del árbol de búsqueda. Pero esto es principalmente intuición, afaik nadie lo ha formalizado con mucho cuidado para probarlo en conjuntos de datos SAT. Ejecutar un solucionador SAT en uno de estos conjuntos de datos no es barato, y mucho menos compararlo con las decisiones óptimas (extensión más pequeña de la asignación actual a variables que violarían una de las cláusulas). VSIDS también depende de qué variables topamos en cada conflicto, hay varias formas de definir cuándo una variable está involucrada en un conflicto.


Hay resultados que muestran que la implementación particular de estas ideas corresponde a una centralidad de vértices ponderada en el tiempo en gráficos dinámicos.

También hay sugerencias de que excluir instancias adversas como las basadas en problemas NP-hard y cripto primitivas e instancias aleatorias (en las que los solucionadores CDCL SAT no son buenos) el resto de instancias provienen de cosas muy bien estructuradas como la verificación de software y hardware y de alguna manera estas los solucionadores de CDCL SAT explotan las estructuras (se han mencionado muchas ideas como puertas traseras, variables congeladas, etc.) pero afaik son en su mayoría ideas y no tienen una fuerte evidencia teórica o experimental que las respalde. Creo que uno tendría que definir rigurosamente el puño correctamente y mostrar que las instancias en las que funcionan bien estos algoritmos tienen la propiedad y luego mostrar que estos algoritmos explotan esas propiedades.


Algunas personas siguen insistiendo en que la relación de cláusula y los umbrales son el único juego en la ciudad. Eso es definitivamente falso, como lo sabría cualquiera que esté un poco familiarizado con el funcionamiento de los solucionadores de SAT industriales o que tenga algún conocimiento de la complejidad de la prueba. Hay muchas cosas que hacen que un solucionador SAT funcione bien o no en una instancia en la práctica y la relación de cláusula es solo una de las cosas que podrían estar involucradas. Creo que la siguiente encuesta es un buen punto de partida para aprender sobre las conexiones entre la complejidad de la prueba y los solucionadores de SAT y la perspectiva:

Curiosamente, incluso el fenómeno del umbral es más complicado de lo que la mayoría de la gente piensa, Moshe Vardi declaró en su charla " Transiciones de fase y complejidad computacional " que el tiempo medio de ejecución de GRASP sigue siendo exponencial para fórmulas aleatorias 3SAT después del umbral, pero que el exponente disminuye (afaik, no está claro qué tan rápido disminuye).


¿Por qué estamos estudiando solucionadores SAT (como teóricos de la complejidad)? Creo que la respuesta es la misma que para otros algoritmos: 1. compararlos, 2. encontrar sus limitaciones, 3. diseñar mejores, 4. responder preguntas fundamentales de la teoría de la complejidad.

Cuando modelamos una heurística, a menudo reemplazamos la heurística con el no determinismo. La pregunta entonces es si es un reemplazo "justo". Y aquí por justo quiero decir qué tan cerca está el modelo para ayudarnos a responder la pregunta anterior.

Cuando modelamos un solucionador SAT como un sistema de prueba, estamos mostrando en parte su limitación porque el algoritmo será ineficiente para las declaraciones que tienen límites más bajos en el sistema de prueba. Pero todavía hay una brecha entre lo que el algoritmo realmente encuentra y la prueba óptima en el sistema de prueba. Por lo tanto, debemos mostrar que también lo contrario, es decir, el algoritmo puede encontrar pruebas que sean tan buenas como las del sistema de pruebas. No estamos cerca de responder esa pregunta, pero la cantidad de heurística que se reemplaza por no determinismo define qué tan cerca está el modelo del sistema de prueba. No espero que descartemos por completo el reemplazo de la heurística con el no determinismo, de lo contrario obtendríamos resultados de automatización que tienen consecuencias en problemas abiertos en criptografía, etc.

Entonces, la pregunta al mirar un modelo es: ¿cuánto ayudan los modelos a explicar por qué el solucionador SAT A es mejor que el solucionador SAT B? ¿Qué tan útiles son para desarrollar mejores solucionadores SAT? ¿El solucionador SAT encuentra pruebas en la práctica que están cerca de las pruebas óptimas en el modelo? ... También necesitamos modelar las instancias prácticas.

En cuanto a la intuición de que los solucionadores de CDCL SAT "explotan la estructura de instancias prácticas" (cualquiera que sea esa estructura) es una intuición generalmente aceptada, creo. La verdadera pregunta es dar una explicación convincente de lo que eso significa y demostrar que es realmente cierto.

Ver también la propia respuesta de Jakob Nordstrom para desarrollos más recientes.

Kaveh
fuente
1
¿Esto es válido para las instancias SAT derivadas de la factorización de enteros?
Mohammad Al-Turkistany
1
heuristicheuristics
Tayfun Pay
1
@ Martin, sin CDCL solo obtenemos formas de resolución muy restringidas (no recuerdo exactamente qué de mi cabeza). Estos son los resultados de Paul Beame y otros que muestran que con CDCL y reinicios esencialmente puede obtener cualquier prueba de resolución general (sin embargo, la selección de puntos de reinicio y ramas son algo artificiales), consulte el documento de Beame para más detalles.
Kaveh
3
@ Martin, vea también la encuesta de Jakob Nordstrom: csc.kth.se/~jakobn/project-proofcplx/docs/…
Kaveh
1
Con respecto a la complejidad de la prueba y el CDCL, Pipatsrisawat y Darwiche mostraron que sciencedirect.com/science/article/pii/S0004370210001669 y de forma independiente por Atserias, Fichte y Thurley jair.org/papers/paper3152.html que CDCL visto como un sistema de prueba puede polinomialmente simule la resolución (los documentos presentan resultados diferentes, pero las pruebas en ambos documentos pueden usarse para obtener los resultados en el otro documento). Una diferencia importante con respecto a trabajos anteriores en esta línea de investigación es que no hay nada articular en estos modelos de CDCL. [Continuará ...]
Jakob Nordstrom
17

Estoy escribiendo esto bastante rápido debido a limitaciones de tiempo severas (y ni siquiera pude responder antes por la misma razón), pero pensé que al menos trataría de contribuir con mis dos centavos.

Creo que esta es una gran pregunta, y he pasado una cantidad de tiempo no trivial en los últimos años investigando esto. (Divulgación completa: he recibido una gran parte de mi financiación actual precisamente para tratar de encontrar respuestas a preguntas de este tipo, y luego potencialmente para convertir información más profunda en SAT en solucionadores SAT más eficientes).

Si uno tuviera que dar una respuesta de una oración, entonces creo

nadie lo sabe realmente y esta es un área activa de investigación

es casi tan bueno como parece. Excepto que hay mucho más espacio para más actividad, especialmente desde el lado de la teoría.

Algunas explicaciones propuestas (no mutuamente excluyentes), que ya se han discutido en otras respuestas y comentarios, son

  • (a) puertas traseras,
  • (b) consideraciones de complejidad parametrizadas,
  • (c) estructura gráfica del problema CNF,
  • (d) consideraciones de complejidad de la prueba, y
  • (e) transiciones de fase.

Comenzando desde el final (e), parece haber bastante confusión con respecto a las transiciones de fase. La respuesta corta aquí es que no hay razón alguna para creer que la relación de cláusulas a variables sea relevante para problemas aplicados o problemas combinatorios teóricos (también conocidos como instancias diseñadas). Pero por alguna razón, es una idea errónea no muy infrecuente en la parte aplicada de la comunidad SAT que la relación de cláusulas a variables debería de alguna manera ser una medida generalmente relevante. La relación cláusula-variable es muy relevante para k-SAT aleatorio, pero no para otros modelos.

Mi sensación es que las puertas traseras (a) han sido una explicación popular, pero personalmente no he visto evidencia convincente de que explique lo que sucede en la práctica.

La complejidad parametrizada (b) proporciona una hermosa teoría sobre algunos aspectos de SAT, y una hipótesis muy atractiva es que las instancias de SAT son fáciles porque tienden a estar "cerca de alguna isla de trazabilidad". Creo que esta hipótesis abre muchas direcciones interesantes de investigación. Como se señaló en algunas de las respuestas, hay muchas conexiones entre (a) y (b). Sin embargo, hasta ahora no veo ninguna evidencia de que la complejidad parametrizada se correlacione demasiado con lo que está sucediendo en la práctica. En particular, parece que las instancias que son manejables pueden ser muy, muy difíciles en la práctica, y las instancias sin puertas traseras pequeñas pueden ser muy fáciles.

La explicación que me parece más creíble para las instancias industriales es (c), a saber, que la estructura (gráfica) de las fórmulas CNF en cuestión debería estar correlacionada con el rendimiento práctico del SAT. La idea aquí es que las variables y cláusulas de instancias industriales pueden agruparse en comunidades bien conectadas con pocas conexiones entre ellas, y que los solucionadores de SAT de alguna manera explotan esta estructura. Desafortunadamente, parece bastante difícil precisar esto de manera más rigurosa, e igualmente desafortunadamente esta área sufre de una buena cantidad de publicidad. Las explicaciones propuestas que he visto hasta ahora en los documentos son bastante insatisfactorias y los modelos parecen ser fáciles de derribar. El problema parece ser que si uno realmente quiere hacer esto a fondo, entonces las matemáticas se ponen realmente difíciles (porque es un problema difícil) y también se vuelven extremadamente desordenadas (porque necesitas que tu modelo esté lo suficientemente cerca de la realidad para obtener resultados relevantes). En particular, los documentos que he visto que explican que el rendimiento de la heurística VSIDS (variable decreciente independiente del estado variable) para elecciones variables funciona bien porque explora las comunidades en la representación gráfica de las instancias son bastante poco convincentes, aunque la hipótesis como tal todavía es muy atractivo.

Una línea de investigación que he seguido personalmente es si el rendimiento práctico del SAT de alguna manera se correlaciona con las medidas de complejidad de prueba de las fórmulas CNF en cuestión. Desafortunadamente, la respuesta corta parece ser que realmente no hay una conexión clara y convincente. Todavía podría ser que hay correlaciones no triviales (esto es algo que estamos investigando actualmente de diferentes maneras), pero parece que la teoría es demasiado agradable, limpia y bonita, y la realidad es demasiado complicada para que haya una buena combinación. (Con respecto al artículo sobre pruebas de medidas de complejidad de prueba y dureza práctica de SATpor Järvisalo, Matsliah, Nordström y Živný en CP '12 resultó que los experimentos más detallados proporcionan una imagen mucho más compleja con conclusiones menos claras --- esperamos llegar a una versión de revista completa que informe sobre esto en cualquier década ahora, pero es complicado, aunque todavía es de esperar interesante).

Otra línea de trabajo relacionada en la complejidad de la prueba es modelar solucionadores SAT de última generación como sistemas de prueba y demostrar teoremas en estos modelos para deducir las propiedades de los solucionadores correspondientes. Sin embargo, esto es un campo de minas, ya que las elecciones de diseño pequeñas y aparentemente inocuas en el lado del modelo teórico pueden llevar a que los resultados sean completamente irrelevantes desde un punto de vista práctico. Por otro lado, si uno quiere un modelo teórico que esté lo suficientemente cerca de la realidad como para dar resultados relevantes, entonces este modelo se vuelve extremadamente desordenado. (Esto se debe a que el rendimiento del solucionador SAT depende de la historia global de todo lo que ha sucedido hasta ahora de manera no trivial, y esto significa que el modelo no puede ser modular en la forma en que usualmente configuramos nuestros sistemas de prueba, ya sea que un paso de derivación en particular sea "correcto"

Sin embargo, dos documentos que realmente deberían mencionarse como excepciones a esto son [Pipatsrisawat y Darwiche 2011] y [Atserias, Fichte y Thurley 2011], donde se muestra que las cláusulas basadas en conflictos que aprenden solucionadores SAT modelados de forma natural tienen el potencial para simular polinomialmente una resolución general completa. Hay una lista bastante larga de documentos que preceden a [PD11] y [AFT11] que esencialmente reclaman el mismo resultado, pero todos tienen serios problemas con el modelado. (Es cierto que [PD11] y [AFT11] también necesitan algunas suposiciones para funcionar, pero son prácticamente las mínimas que esperaría a menos que solicite documentos que también muestren que la jerarquía de complejidad parametrizada colapsa).

Una vez más, estoy escribiendo todo esto muy rápido, pero si hay un interés sustancial por algo de lo anterior, podría intentar elaborarlo (aunque podría llevar un tiempo volver a esto de nuevo --- por favor, siéntase libre de enviarme un ping si hay es cualquier cosa que quieras que comente). Como una forma rápida de proporcionar referencias, permítanme hacer algunos autoenchufes descarados (aunque la vergüenza disminuye un poco cuando veo que algunos comentarios también han citado algunas de estas referencias):

Charla estilo tutorial sobre la interacción entre la complejidad de la prueba y la solución SAT ofrecida en la Escuela Internacional de Verano sobre Teoría del Módulo de Satisfacción, Satisfabilidad y Razonamiento Automatizado en 2016 con muchas referencias completas al final de las diapositivas: http://www.csc .kth.se / ~ jakobn / research / TalkInterplaySummerSchool2016.pdf

Charla de encuestas un poco más reciente y más breve Comprensión de la resolución de conflictos impulsada por el conflicto a través de la lente de la complejidad de la prueba desde principios de 2017 (también con referencias completas al final): http://www.csc.kth.se/~jakobn/research /TalkProofComplexityLensCDCL1702.pdf

Encuesta de conexiones entre la complejidad de la prueba y la resolución SAT: http://www.csc.kth.se/~jakobn/research/InterplayProofCplxSAT.pdf [Referencia bibliográfica: Jakob Nordström. Sobre la interacción entre la complejidad de la prueba y la resolución SAT. ACM SIGLOG News, volumen 2, número 3, páginas 19-44, julio de 2015. (Versión ligeramente editada con algunos errores tipográficos corregidos)]

Documento SAT '16 con CDCL modelado fielmente como un sistema de prueba: http://www.csc.kth.se/~jakobn/research/Trade-offsTimeMemoryModelCDCL_SAT.pdf [Referencia bibliográfica: Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard , Jakob Nordström y Marc Vinyals. Compromisos entre tiempo y memoria en un modelo más estricto de solucionadores CDCL SAT. En Actas de la XIX Conferencia Internacional sobre Teoría y Aplicaciones de Pruebas de Satisfacción (SAT '16), Lecture Notes in Computer Science, volumen 9710, páginas 160-176, julio de 2016.]

Jakob Nordstrom
fuente
16

Permítanme agregar mis dos centavos de comprensión a esto, a pesar de que nunca he trabajado en el área.

Estás haciendo una de dos preguntas, "¿cuáles son todos los enfoques conocidos para probar la eficiencia teórica de algún solucionador SAT para algún tipo de instancias" y "por qué los solucionadores SAT son eficientes en la realidad".

Para la primera pregunta, lo dirigiré a la investigación de Stefan Szeider. Me parece ser el área más activa actualmente en el tema de las puertas traseras y las parametrizaciones FPT de SAT (que incluye tanto enfoques estructurales como medidas de tipo árbol-ancho y los llamados conjuntos de puerta trasera, así como alguna mezcla de los dos).

Para la última pregunta, para ser honesto, esa pregunta exacta se ha debatido en todos los talleres de resolución de SAT a los que he asistido (incluidos los últimos años), por lo que no es un asunto resuelto. Pero mi impresión es la siguiente.

En primer lugar, debe cuantificar o restringir lo que quiere decir con "en realidad". No es cierto que los solucionadores SAT sean solucionadores universalmente buenos para cualquier problema que les plantees (por supuesto), y entre diferentes problemas terminas necesitando diferentes estrategias. Por ejemplo, hay varios éxitos recientes en los que las conjeturas matemáticas han sido verificadas o ajustadas por una enorme búsqueda por computadora ayudada por un solucionador de SAT. En este caso, al parecer, muchas veces las inteligentes mejoras y la heurística de estilo CDCL que los solucionadores modernos de SAT normalmente emplean realmente no le dan demasiada potencia, y el juego se reduce a una forma inteligente de dividir su problema fuente en partes, seguido de (esencialmente) un algoritmo de ramificación de fuerza bruta con un pequeño factor constante en el tiempo de ejecución.

Puede que este punto esté sobrevendiendo un poco, pero mi punto fue que, cuando los solucionadores de SAT atacaron, por ejemplo, la Conjetura de Discrepancia de Erdos, tuvieron éxito por una razón diferente a cuando resolvieron instancias industriales derivadas de pruebas de circuito.

Entonces nos preguntamos, ¿por qué los solucionadores basados ​​en CDCL funcionan tan bien en instancias industriales de, por ejemplo, verificación de circuitos (prueba de equivalencia de circuitos)? Yo piensoque la visión más poderosa (o la vista de consenso) aquí es la estrategia de búsqueda de un CDCL que resuelve muy bien los geles con la estructura de estas instancias. Esto significa, por ejemplo, que los circuitos consisten en partes relativamente complejas (llamadas agrupaciones), interconectadas por relativamente pocas conexiones y conexiones más simples, posiblemente de manera jerárquica; y que los solucionadores de CDCL con todas sus heurísticas son muy buenos para explotar (de facto) esto y "proyectar" estos grupos en las variables compartidas, de cualquier forma u orden que sea más útil para verificar el circuito en cuestión. Pero también parece ser la opinión de consenso de que esta es una explicación insuficiente (por ejemplo, probablemente no podamos explicar teóricamente la eficiencia de los solucionadores CDCL SAT en este dominio simplemente al referirnos a la estructura gráfica de la instancia).

Entonces, ¿las parametrizaciones manejables ayudan a explicar esto último? Para ser sincero, no lo sé. Creo que probablemente haya un efecto poderoso en juego de que las instancias del mundo real no son el peor de los casos, ni son (probablemente) un caso realmente promedio de acuerdo con cualquier distribución de instancias que podamos manejar. Pero probablemente todavía valga la pena preguntar.

Magnus Wahlström
fuente
2
Magnus, definitivamente tienes más experiencia en esta área que cualquier otra persona que haya intentado responder esta pregunta hasta ahora. Cuando dije "mis dos centavos", me refería al hecho de que solo había estudiado un grupo específico de problemas NP-Complete en mi disertación y cómo los solucionadores de CSP y SAT intentan resolver los numerosos casos de estos problemas. También tengo aproximadamente un año de experiencia en el uso de solucionadores CSP y SAT en el lugar de trabajo, pero una vez más, eso ni siquiera está cerca de sus más de 10 años de experiencia en este campo. Sus "dos centavos" probablemente valen "dos pepitas de oro". Una pregunta.
Tayfun Pay
1
Usted declara lo siguiente en su respuesta "No es cierto que los solucionadores SAT sean solucionadores universalmente buenos para cualquier problema que les presente ...". ¿Pudiste ver la relación de cláusulas a variables, c = m / n, para estos casos? En otras palabras, ¿estaban en la región difícil, c = ~ 4.2 o no? Debido a que lo que he experimentado es que terminas con muchas variables cuando reduces una instancia de CSP a una instancia de SAT, y generalmente se debe a esa razón y no porque en realidad está en la región difícil, el solucionador de SAT tarda más hora de resolver
Tayfun paga el
1
Por otro lado, si sabe que estas instancias terminaron en la región difícil de SAT, c = ~ 4.2, ¿puedo saber cuál fue este problema de la vida real? Me interesaría mucho saber qué problemas de la vida real realmente terminan en la región difícil del SAT cuando se reducen a él. Gracias
Tayfun Pay
2
Honestamente, tengo poca o ninguna experiencia en la resolución práctica de SAT. Todo mi trabajo real ha estado en el lado de la teoría pura de esa pregunta. Pero sea como sea, con respecto a su pregunta: mi impresión es que los resultados para k-SAT aleatorio y la densidad de cláusula (que usted menciona) realmente solo se aplican si su instancia de entrada es literalmente una fórmula uniformemente aleatoria. También tenga en cuenta que el límite ~ 4.2 solo se aplica si la fórmula es 3-SAT, a diferencia de una fórmula CNF de longitud mixta.
Magnus Wahlström
1
Y por "problemas que los solucionadores SAT no resuelven bien", me refiero principalmente a problemas que se presume que son realmente intratables, como romper una buena criptografía. Sin embargo, también hay fórmulas que ningún solucionador de CDCL podrá resolver de manera eficiente debido a los límites inferiores teóricos de la prueba, como las fórmulas de principio de agujero de paloma. He visto al menos una conversación con el mensaje "Los solucionadores de CDCL SAT me fallaron", donde un poco de excavación revela que su codificación de problemas oculta un aspecto parecido a un agujero de paloma (por ejemplo, que contiene alguna variación del problema de asignación). Desafortunadamente, no puedo recordar los detalles.
Magnus Wahlström
15

Matti Järvisalo, Arie Matsliah, Jakob Nordström y Stanislav Živný en CP '12 tienen un documento titulado " Medidas de complejidad de prueba relacionadas y dureza práctica de SAT ", que intenta vincular la dureza o la facilidad de resolver ciertas fórmulas mediante solucionadores de CDCL con prueba de resolución medidas de complejidad, en particular el espacio de prueba de resolución. Los resultados son algo mixtos, pero creo que es un paso en la dirección correcta.

Jan Johannsen
fuente
Desafortunadamente, la respuesta corta parece ser que realmente no hay una conexión clara y convincente para probar las medidas de complejidad. Todavía podría ser que hay correlaciones no triviales, pero parece que la teoría es demasiado clara y la realidad es demasiado desordenada para que haya una buena coincidencia. Con respecto al documento "Relacionando las medidas de complejidad de la prueba", resultó que los experimentos más detallados proporcionan una imagen mucho más compleja con conclusiones menos claras --- esperamos llegar a una versión de revista completa que informe sobre esto en cualquier década, pero es complicado , aunque todavía espero que sea interesante.
Jakob Nordstrom
15

No soy un experto en esta área, pero creo que el material de transición aleatorio SAT / fase no está relacionado en absoluto con las aplicaciones industriales / prácticas.

Por ejemplo, los muy buenos solucionadores para instancias aleatorias (como https://www.gableske.net/dimetheus ) se basan en los métodos de física estadística (propagación de creencias, etc.), creo, mientras que los muy buenos solucionadores 'generales' (como como http://fmv.jku.at/lingeling/ ) están utilizando técnicas no relacionadas (más bien de lo que Kaveh estaba hablando) creo.

Pero, como dije, tal vez no confíes en mi palabra; Esto viene de un no experto definido.

Ryan O'Donnell
fuente
Sí. El SAT aleatorio y el SAT industrial son juegos completamente diferentes, y los métodos utilizados son diferentes. Y, además, si desea resolver casos combinatorios realmente difíciles, entonces otras técnicas son más exitosas (por ejemplo, si el problema es lo suficientemente difícil, entonces el aprendizaje de la cláusula realmente no vale la pena, excepto quizás muy localmente). Pero de alguna manera parece una idea errónea bastante común (al menos en el lado aplicado de la comunidad SAT) que la proporción de cláusulas a variables debería de alguna manera ser relevante para cualquier instancia SAT de CNF y no solo para instancias aleatorias.
Jakob Nordstrom