SAT es el problema de determinar si una expresión booleana puede hacerse realidad. Por ejemplo, (A) puede hacerse realidad estableciendo A = VERDADERO, pero (A &&! A) nunca puede ser verdad. Se sabe que este problema es NP-completo. Ver satisfacción booleana .
Su tarea es escribir un programa para SAT que se ejecute en tiempo polinómico, pero que no resuelva todos los casos.
Para algunos ejemplos, la razón por la que no es realmente polinomial podría ser porque:
- Hay un caso límite que no es obvio pero tiene un tiempo de ejecución deficiente
- El algoritmo en realidad no resuelve el problema en algún caso inesperado
- Algunas características del lenguaje de programación que está utilizando en realidad tienen un tiempo de ejecución más largo de lo que razonablemente esperaría que tuviera.
- Su código en realidad hace algo totalmente diferente de lo que parece que está haciendo.
Puede usar cualquier lenguaje de programación (o combinación de idiomas) que desee. No necesita proporcionar una prueba formal de la complejidad de su algoritmo, pero al menos debe proporcionar una explicación.
El criterio principal para juzgar debería ser qué tan convincente es el código.
Este es un concurso de popularidad, por lo que gana la respuesta mejor calificada en una semana.
fuente
Respuestas:
C#
"Aparece" es innecesario. Puedo escribir un programa que realmente se ejecute en tiempo polinómico para resolver problemas SAT. Esto es bastante sencillo de hecho.
Increíble. Por favor envíeme el millón de dólares. En serio, tengo un programa aquí que resolverá SAT con tiempo de ejecución polinómico.
Permítanme comenzar diciendo que voy a resolver una variación del problema SAT. Voy a demostrar cómo escribir un programa que exhiba la solución única de cualquier problema de 3-SAT . La valoración de cada variable booleana debe ser única para que mi solucionador funcione.
Comenzamos declarando algunos métodos y tipos de ayuda simples:
Ahora escojamos un problema de 3 SAT para resolver. Digamos
Hagamos un paréntesis de eso un poco más.
Codificamos eso así:
Y, efectivamente, cuando ejecutamos el programa, obtenemos una solución para 3-SAT en tiempo polinómico. De hecho, el tiempo de ejecución es lineal en el tamaño del problema .
fuente
Multi-idioma (1 byte)
El siguiente programa, válido en muchos idiomas, principalmente funcional y esotérico, dará la respuesta correcta para una gran cantidad de problemas SAT y tiene una complejidad constante (!!!):
Sorprendentemente, el próximo programa dará la respuesta correcta para todos los problemas restantes y tiene la misma complejidad. ¡Entonces solo necesita elegir el programa correcto, y tendrá la respuesta correcta en todos los casos!
fuente
JavaScript
¡Al usar el no determinismo iterado, SAT se puede resolver en tiempo polinómico!
Ejemplo de uso:
Por cierto, estoy orgulloso de haber tenido la oportunidad de utilizar dos de las funciones menos utilizadas de JavaScript, una al lado de la otra:
eval
ywith
.fuente
1000
en el bucle for debería escalar de alguna manera con el tamaño de entrada (alguna escala polinómica no-O (1)).Matemática + Computación Cuántica
Es posible que no sepa que Mathematica viene con una computadora cuántica a bordo
La conmutación adiabática cuántica codifica un problema a resolver en un hamiltoniano (operador de energía) de tal manera que su estado de energía mínima ("estado fundamental") represente la solución. Por lo tanto, la evolución adiabática de un sistema cuántico al estado fundamental del hamiltoniano y la medición posterior da la solución al problema.
Definimos un subhamiltoniano que corresponde a
||
partes de la expresión, con la combinación apropiada de operadores de Pauli para variables y su negación.Donde para una expresión como esta
el argumento debería verse así
Aquí está el código para construir dicho argumento a partir de la expresión bool:
Ahora construimos un Hamiltoniano completo, resumiendo los subhamiltonianos (la suma corresponde a
&&
partes de la expresión)Y busca el estado de energía más bajo
Si tenemos un valor propio de cero, entonces el vector propio es la solución
fuente
Aquí hay tres enfoques, todos implican una reducción de SAT en su lingua franca geométrica 2D: rompecabezas de lógica de nonogramas. Las celdas en el rompecabezas lógico corresponden a variables SAT, restricciones a cláusulas.
Para obtener una explicación completa (¡y para revisar mi código en busca de errores!), Ya publiqué algunas ideas sobre los patrones dentro del espacio de solución de nonogramas. Ver https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space. Enumerar> 4 mil millones de soluciones de rompecabezas y codificarlas para que encajen en una tabla de verdad muestra patrones fractales: auto-similitud y especialmente autoafinidad. Esta redundancia afín demuestra la estructura dentro del problema, explotable para reducir los recursos computacionales necesarios para generar soluciones. También muestra la necesidad de retroalimentación caótica dentro de cualquier algoritmo exitoso. Existe un poder explicativo en el comportamiento de transición de fase donde las instancias "fáciles" son aquellas que se encuentran a lo largo de la estructura gruesa, mientras que las instancias "duras" requieren una mayor iteración en detalles finos, bastante ocultas de la heurística normal. Si desea ampliar la esquina de esta imagen infinita (todas las instancias de rompecabezas <= 4x4 codificadas) consulte http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html
Método 1. Extrapolar la sombra espacial de la solución de nonogramas utilizando mapas caóticos y aprendizaje automático (piense en funciones de ajuste similares a las que generan el conjunto de Mandelbrot).
Aquí hay una prueba visual de inducción. Si puede escanear estas cuatro imágenes de izquierda a derecha y piensa que tiene una buena idea para generar la quinta falta ... etc ... sexta imágenes, entonces me acaba de programar que como mi oráculo NP para el problema de decisión de la solución nonogram existencia. Da un paso adelante para reclamar tu premio como la supercomputadora más poderosa del mundo. Te alimentaré con descargas eléctricas de vez en cuando mientras el mundo te agradece por tus contribuciones computacionales.
Método 2. Utilice transformadas de Fourier en la versión de imagen booleana de las entradas. Los FFT proporcionan información global sobre frecuencia y posición dentro de una instancia. Si bien la porción de magnitud debe ser similar entre el par de entrada, su información de fase es completamente diferente, ya que contiene información direccionalizada sobre una proyección de solución a lo largo de un eje específico. Si es lo suficientemente inteligente, puede reconstruir la imagen de fase de la solución a través de una superposición especial de las imágenes de fase de entrada. Luego, invierta la transformación de la fase y la magnitud común de vuelta al dominio del tiempo de la solución.
¿Qué podría explicar este método? Hay muchas permutaciones de las imágenes booleanas con relleno flexible entre ejecuciones contiguas. Esto permite un mapeo entre la entrada -> solución cuidando la multiplicidad mientras conserva la propiedad de FFT de mapeos bidireccionales y únicos entre el dominio del tiempo <-> (frecuencia, fase). También significa que no existe tal cosa como "no hay solución". Lo que diría es que, en un caso continuo, existen soluciones en escala de grises que no está considerando al mirar la imagen de dos niveles de la resolución tradicional de rompecabezas de nonogramas.
¿Por qué no lo harías? Es una forma horrible de calcular, ya que las FFT en el mundo de punto flotante de hoy en día serían muy inexactas con grandes instancias. La precisión es un gran problema, y la reconstrucción de imágenes a partir de imágenes cuantificadas de magnitud y fase generalmente crea soluciones muy aproximadas, aunque tal vez no sea visualmente para los umbrales del ojo humano. También es muy difícil llegar a este negocio de superposición, ya que actualmente se desconoce el tipo de función que lo realiza. ¿Sería un simple esquema de promedio? Probablemente no, y no hay un método de búsqueda específico para encontrarlo, excepto la intuición.
Método 3. Encuentre una regla de autómatas celulares (de un posible ~ 4 mil millones de tablas de reglas para las reglas de 2 estados de von Neumann) que resuelve una versión simétrica del rompecabezas de nonogramas. Utiliza una incrustación directa del problema en las celdas, como se muestra aquí.
Este es probablemente el método más elegante, en términos de simplicidad y buenos efectos para el futuro de la informática. La existencia de esta regla no está probada, pero tengo el presentimiento de que existe. Este es el por qué:
Los nonogramas requieren muchos comentarios caóticos en el algoritmo para ser resueltos exactamente. Esto se establece mediante el código de fuerza bruta vinculado a la Revisión de código. CA es el lenguaje más capaz para programar comentarios caóticos.
Se ve bien, visualmente. La regla evolucionaría a través de una incrustación, propagaría la información horizontal y verticalmente, interferiría y luego se estabilizaría en una solución que conservara el número de celdas establecidas. Esta ruta de propagación sigue el camino (hacia atrás) en el que normalmente piensa cuando proyecta la sombra de un objeto físico en la configuración original. Los nonogramas se derivan de un caso especial de tomografía discreta, así que imagínese sentado al mismo tiempo en dos escáneres de CT acorralados por gatitos ... así es como se propagarían los rayos X para generar las imágenes médicas. Por supuesto, hay problemas de límites: los bordes del universo CA no pueden seguir propagando información más allá de los límites, a menos que permita un universo toroidal. Esto también arroja el rompecabezas como un problema periódico de valor límite.
Explica múltiples soluciones como estados transitorios en un efecto oscilante continuo entre el intercambio de salidas como entradas, y viceversa. Explica instancias que no tienen solución como configuraciones originales que no conservan el número de celdas establecidas. Dependiendo del resultado real de encontrar dicha regla, incluso puede aproximarse a instancias insolubles con una solución cercana donde se conservan los estados celulares .
fuente
C ++
Aquí hay una solución que se garantiza que se ejecutará en tiempo polinómico: se ejecuta en
O(n^k)
donden
está el número de booleanos yk
es una constante de su elección.fuente
bitfield
, tal vez hubiera preferido esostd::vector
.ruby / gnuplot superficie 3d
(¡oh, dura competencia!) ... de todos modos ... ¿una imagen vale más que mil palabras? Estas son 3 gráficas de superficie separadas hechas en gnuplot del punto de transición SAT. los ejes (x, y) son cláusula y recuento variable y la altura z es el número total de llamadas recursivas en el solucionador. Código escrito en rubí. Muestra 10x10 puntos a 100 muestras cada uno. Demuestra / usa principios básicos de estadística y es una simulación de Monte Carlo .
es básicamente un algoritmo de davis putnam que se ejecuta en instancias aleatorias generadas en formato DIMACS. Este es el tipo de ejercicio que idealmente se realizaría en las clases de CS en todo el mundo para que los estudiantes puedan aprender los conceptos básicos, pero casi no se les enseña específicamente ... ¿tal vez alguna razón por la que hay tantas pruebas falsas de P? = NP ? ni siquiera hay un buen artículo de wikipedia que describa el fenómeno del punto de transición (¿hay quienes lo tomen?) que es un tema muy destacado en física estadística y también es clave en CS. [a] [b] hay muchos artículos en CS sobre el punto de transición ¡Sin embargo, muy pocos parecen mostrar gráficos de superficie! (en su lugar, generalmente muestra rodajas en 2D).
El aumento exponencial en el tiempo de ejecución es claramente evidente en la primera parcela. El sillín que corre por el medio de la primera parcela es el punto de transición. los 2 nd y 3 rd gráficos muestran la transición satisfiable%.
[a] comportamiento de transición de fase en CS ppt Toby Walsh
[b] probabilidad empírica de satisfacción de k-SAT tcs.se
[c] grandes momentos en matemática empírica / experimental / (T) CS / SAT , blog TMachine
fuente