Curioso acerca de las pruebas de integridad de NP asistidas por computadora

En el artículo "LA COMPLEJIDAD DE LOS PROBLEMAS DE SATISFIABILIDAD" de Thomas J. Schaefer, el autor ha mencionado que

This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.

Por supuesto, esto es una limitación:

The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.

Tengo curiosidad de que

1. ¿Existen investigaciones de seguimiento en el desarrollo de esta idea de "pruebas de integridad de NP asistidas por computadora"? ¿Cuál es el estado del arte (puede ser específico de o )? Dado que Schaefer ha propuesto la idea de la prueba de integridad de NP "asistida por computadora" (al menos para las reducciones de ), esto significa que hay algunos principios / estructuras generales subyacentes a estas reducciones (para las de \ textf { 3SAT} o \ text {3-Partition} )? Si es así, ¿Que son? 3-Partition SAT 3SAT$\textsf{3SAT}$$\textsf{3-Partition}$
   $\textsf{SAT}$$\textsf{3SAT}$$\text{3-Partition}$
2. ¿Alguien tiene experiencia en probar la completitud NP con un asistente de computadora? ¿O alguien puede inventar un ejemplo artificial?

En cuanto a la pregunta 2, hay al menos dos ejemplos de pruebas de completitud que involucran a un asistente de computadora.$NP$

Erickson y Ruskey proporcionaron una prueba asistida por computadora de que Domino Tatami Covering es NP-complete. Dieron una reducción de tiempo polinomial de 3-SAT planas a tatami dominó cubriendo. Se utilizó un solucionador SAT (Minisat) para automatizar el descubrimiento de dispositivos en la reducción. Ninguna otra prueba de completitud es conocida por ello.$NP$

Ruepp y Holzer demostraron que el rompecabezas de lápiz Kakuro es completo. Algunas partes de la prueba de completitud se generaron automáticamente utilizando un solucionador SAT (de nuevo Minisat).N $NP$$NP$

En este artículo, mostré que si para algunos hay un gráfico con un grado máximo y una fuerza cromática del borde estrictamente mayor que , entonces es -completo para decidir si la fuerza cromática del borde es como máximo . Tales gráficos eran conocidos para e hice una búsqueda en la computadora para encontrar un gráfico de vértices adecuado para .$k\geq 3$k Θ p 2 k k > 3 12 k = $k$$k$$\Theta_2^p$$k$$k>3$$12$$k=3$

La complejidad de la resistencia cromática y la resistencia cromática del borde. Complejidad computacional, 14 (4): 308-340, 2006

Del comentario anterior:

Utilicé la biblioteca Choco Java para la programación de restricciones para verificar el comportamiento correcto de los gadgets utilizados para demostrar la integridad de NP de los siguientes rompecabezas: rompecabezas binario, carpas, rompecabezas de cubo rodante sin celdas libres, red. Todavía no tuve tiempo de publicarlos, pero los borradores están disponibles en mi blog.

La técnica utilizada es similar: todos esos rompecabezas se pueden modelar como un gráfico de cuadrícula en el que cada nodo puede contener un elemento diferente (por ejemplo, en el rompecabezas binario los elementos son: celda vacía, fijo 0, fijo 1, 0, 1), las reglas del rompecabezas permiten o prohíben algunas configuraciones (locales) (por ejemplo, en el rompecabezas binario no se permiten más de dos so s al lado o debajo del otro). Luego, para probar la completitud de NP es suficiente construir un gadget cuadrado que simule:1 n × $0$$1$$n \times n$

(A) una puerta lógica (AND + OR) y enlaces, si queremos utilizar SAT SATELARO como el problema NPC de origen; o

(B) un nodo de grado 3 en el que exactamente 1 entrada y 1 salida pueden activarse al mismo tiempo, si queremos utilizar el CICLO HAMILTONIANO en los gráficos de cuadrícula como el problema de la fuente NPC (tenga en cuenta que en este caso, debe haber otro condición que fuerza una "ruta conectada").

En ambos casos, utilizamos una configuración inicial que corrige los límites de los gadgets (para prohibir interacciones no deseadas) y permitimos la interacción entre dos gadgets adyacentes solo a través de un elemento central (o grupo de elementos). La configuración de dicho elemento central debe representar un valor lógico en el caso (A) o un recorrido en el caso (B).

Por ejemplo, para modelar un AND:

***C***   *=fixed elements (initial config. of the puzzle)
*xxxxx*   x=internal logic (some elements can be fixed,
AxxxxxB     other must be completed/traversed)
*xxxxx*   A,B,C=elements shared with adjacent gadgets
*******

En este punto, para verificar el dispositivo con un solucionador SAT (es mejor usar una CPL), es suficiente para implementar las reglas del rompecabezas, luego verifique la satisfacción cuando A, B, C toman todas las combinaciones posibles de valores; y ver si son consistentes con el comportamiento deseado. Por ejemplo, en el caso AND, en todas las configuraciones válidas (satisfactorias) de gadgets en las que C es verdadero (C representa el valor lógico verdadero), tanto A como B deben ser verdaderas.

Si los gadgets son muy complicados (por ejemplo, en el rompecabezas del cubo rodante), creo que es la única forma de garantizar que funcionen correctamente (y que la prueba de NPC sea correcta).

¡Hice esto mismo, a prueba de integridad NP asistida por computadora, en mi tesis de licenciatura!

Lo malo es que está en ruso y no fue traducido al inglés. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf

Trabajé con puertas lógicas en problemas 2D. El plan es:

• Diseñe manualmente cómo se ve un "cable" en su problema.
• Utilice una búsqueda muy inteligente y optimizada (de hecho, programación dinámica sobre conjuntos de perfiles) para diseñar automáticamente todas las puertas lógicas necesarias.
• ¡LUCRO!

El código está disponible, por cierto: https://code.google.com/p/metadynamic-programming/

De esta manera, con el trabajo manual solo para diseñar el cable y codificar las reglas del problema 2D específico, pude demostrar que NP estaba completo:

• Dragaminas
• Cubriendo el área con dominó horizontal y trimino vertical
• $k$$k \ge 4$$k \in [4,6]$

el interlocutor ha indicado que está de acuerdo con una interpretación más amplia de la declaración de Schaefer en una respuesta. casualmente he estado recopilando enlaces para un blog sobre un tema cercano y escribiré algunos aquí.

la declaración original (sec 7 p225) es clara en sus intenciones, como se ilustra con el ejemplo de una reducción completa de NP de 2 colorantes perfectos thm 7.1 utilizando la "dicotomía thm" 2.1.

$F(x)$

$F(x)$$x$

Tomando un punto de vista amplio, se puede ver que estas ideas generales han crecido y explorado en muchas áreas de investigación desde estas reflexiones de 1978 / "ideas de semillas" que conducen a grandes ramas enteras y programas de investigación, aún en curso, ninguno de los cuales existía en casi ninguna forma Al momento de escribir el artículo de Schaefers. La ^primera idea general es el análisis empírico de las propiedades de completitud de NP a través de generadores / solucionadores / analizadores de instancias .

• El área de investigación más grande engendrada aquí es en instancias SAT aleatorias y observar el rendimiento del solucionador SAT en ellas, lo que condujo al descubrimiento del punto de transición a mediados de la década de 1990, que luego demostró tener profundas conexiones con la física estadística y un aspecto aparentemente ubicuo / intrínseco / fundamental. / característica de todos los problemas completos de NP. Hay muchos documentos en esta área y ahora algunos libros. ver, por ejemplo , información, física y computación Mezard / Montanari

• Descomponiendo los problemas de satisfacción o el uso de gráficos para obtener una mejor visión de los problemas de satisfacción , Herwig 2006 (83pp). Este es un enfoque algo novedoso con otras investigaciones publicadas que analiza la estructura gráfica de cláusula variable de las instancias de SAT generadas y analiza su estructura / métrica para encontrar correlaciones con la dureza.

• uno puede tomar problemas conjeturados y codificarlos como instancias SAT y luego examinar su estructura o ejecutar solucionadores SAT en ellos y observar el comportamiento dinámico de los solucionadores SAT. no es fácil darse cuenta cuando esto se hizo por primera vez, pero un caso temprano es con factoring, probablemente a mediados de la década de 1990 más o menos, y estas instancias aparecieron en los concursos de solución DIMACS SAT. desafortunadamente, esto no fue necesariamente considerado resultados de investigación publicables por separado en ese momento. Hay alusiones en algunos documentos SAT.

  ver, por ejemplo, Satisfacer esto: un intento de resolver la factorización prima utilizando los solucionadores de satisfacción por Stefan Schoenmackers, Anna Cavender y también la pregunta cs.se que reduce el problema de factorización de enteros al problema NP completo y (hay algunas otras preguntas relacionadas / intercambiadas (T) CS stackexchange en esta).

2 ^nd otra idea moderna / semilla generales inherentes Schaefers vieja afirmación es atacar los problemas algorítmicos o matemáticos duros en general mediante la conversión a instancias del SAT, y el uso off-the-shelf (pero por el estado de la técnica) solucionadores SAT (es decir, La resolución SAT puede considerarse en términos generales como uno de los primeros casos en lógica / matemática del teorema automatizado por computadora que demuestra que las soluciones de fórmulas SAT son como "teoremas", aunque es cierto que el punto de vista moderno puede haber cambiado un poco) y hay algunos notables recientes éxitos en este frente.

• El problema de la discrepancia de Erdos relacionado con los límites en las caminatas aleatorias es muy difícil y el progreso fue limitado con enfoques analíticos, y recientemente se adoptó un enfoque empírico novedoso y sin precedentes con SAT para lograr algunos resultados clave en un problema abierto relacionado, celebrado por muchos como un Verdadero avance. un ataque SAT en la conjetura de discrepancia de Erdos Konev, Lisitsa

• La investigación sobre redes de clasificación óptimas se remonta a décadas y existen problemas naturales de difícil acceso en tamaños mínimos de redes para clasificar un número determinado de elementos. En los últimos años ha habido un progreso reciente importante en la conversión de estos a instancias SAT y la ejecución de solucionadores estándar en ellos. Nuevos límites en redes de clasificación óptimas Ehlers, Müller, también cita otros trabajos recientes.