¿Para qué es SAT y para qué es bueno?

Question

Recientemente vi un artículo de Reddit sobre el uso de SAT para resolver un rompecabezas [1]. Esto me consiguió muy curiosos sobre esta cosa de "sat". Leí el artículo de Wikipedia, pero me gustaría pedirle a alguien que me lo explique en términos más laicos.

¿Para qué es SAT y para qué es bueno? ¿Se puede utilizar para atravesar una estructura de árbol? Para analizar textos? Para la ruptura de la línea [2]? Para el embalaje de contenedor [3]? ¿Es un tipo de técnica de optimización?

En la nota relacionada, leí que NP vs P se trata de elegir qué números de una suma establecida a cero frente a verificar si algunos números se suman a cero - ¿Se siente de alguna manera relacionado con esto?

[1] http://www.reddit.com/r/programming/comments/pxpzd/solving_hexiom_really_fast_with_a_sat_solver/

[2] http://en.wikipedia.org/wiki/line_wrap

[3] http://en.wikipedia.org/wiki/bin_packing_problem

Answer 1

SAT es muy importante porque es NP-Completo. Para comprender lo que esto significa que necesita una noción clara de clases de complejidad. Aquí hay un breve resumen:

• P es la clase de todos los problemas que se pueden resolver en el tiempo polinomial (es decir, rápido).

• NP es la clase de todos los problemas para el que se puede verificar una solución en el tiempo polinomial. Esto significa que una solución muy determinada es rápida, pero encontrar una suele ser lenta (con la mayoría de las veces el tiempo exponencial). A menos que el problema esté en la parte P de NP, por supuesto (como se señala a continuación, P es parte de NP, como puede verificar fácilmente).

Luego está el conjunto de problemas completos de NP. Este conjunto contiene todos los problemas que son tan genéricos que puede resolver estos problemas en lugar de otro de NP (esto se llama reducir un problema a otro). Esto significa que puede transformar un problema de un dominio en otro problema completo de NP, hacer que deriva una respuesta y transformar la respuesta.

Sin embargo, a menudo se puede demostrar que un problema es NP-completado, pero las transformaciones no están claras para otro problema dado.

SAT es muy agradable, porque es NP-Completo, es decir, puedes resolverlo en lugar de cualquier otro problema en NP, y también las reducciones no son tan difíciles de hacer. TSP es otro problema completo de NP, pero las transformaciones a menudo son mucho más difíciles.

Entonces, sí, SAT se puede usar para todos estos problemas que está mencionando. A menudo, sin embargo, esto no es factible. Donde es factible es, cuando no se conoce ningún otro algoritmo rápido, como el rompecabezas que menciona. En este caso, no tiene que desarrollar un algoritmo para el rompecabezas, pero puede usar cualquiera de los solucionadores SAT altamente optimizados y terminará con un algoritmo rápido razonable para su rompecabezas.

Atravesar una estructura de árbol es tan simple, por ejemplo, que cualquier transformación y SAT probablemente sea mucho más compleja que simplemente escribir el recorrido directamente.

Answer 2

Para resumir, un solucionador SAT es algo a lo que le das una fórmula booleana, y le dice si puede encontrar un valor para las diferentes variables de modo que la fórmula sea cierta.

Ejemplo

suponer que a, b y c son variables booleanas, y desea saber si a estas variables se les puede asignar un valor que de alguna manera hace la fórmula (¬a ∨ b) ∧ (¬b ∨ c). Envías esta fórmula al solucionador SAT y te devolverá true. Los solucionadores SAT también a menudo le dan una tarea válida. En este caso, esta tarea podría ser a: false, b:false, c:false.

Para qué se puede usar ?

No lo usaría para atravesar árboles ni para analizar el texto o romper las líneas. Sin embargo, podría usarlo al atravesar un árbol para verificar si se satisfacen algunas restricciones en el árbol. Ciertamente, puede usarlo para el embalaje, a pesar de que algunos solucionadores CSP especializados probablemente funcionarán mejor en este tipo de problemas.

Los solucionadores SAT se están volviendo mucho más comunes en estos días, especialmente en software como los administradores de paquetes. Eclipse incorpora SAT4J para administrar las dependencias entre sus complementos. Otras aplicaciones de SAT generalmente incluyen verificación de modelos, aplicaciones de planificación, configuradores, programación y muchos otros.