Reducción directa de SAT a 3-SAT

Aquí el objetivo es reducir un problema SAT arbitrario a 3-SAT en tiempo polinómico usando el menor número de cláusulas y variables. Mi pregunta está motivada por la curiosidad. Menos formalmente, me gustaría saber: "¿Cuál es la reducción 'más natural' de SAT a 3-SAT?"

Ahora la reducción que siempre he visto en los libros de texto es algo así:

1. Primero tome su instancia de SAT y aplique el teorema de Cook-Levin para reducirlo al circuito SAT.

2. Luego termina el trabajo mediante la reducción estándar del circuito SAT a 3-SAT reemplazando las compuertas con cláusulas.

Si bien esto funciona, las cláusulas 3-SAT resultantes no se parecen en nada a las cláusulas SAT con las que comenzó, debido a la aplicación inicial del teorema de Cook-Levin.

¿Alguien puede ver cómo hacer la reducción más directamente, omitiendo el paso del circuito intermedio y yendo directamente a 3-SAT? Incluso estaría contento con una reducción directa en el caso especial de n-SAT.

(Supongo que hay algunas compensaciones entre el tiempo de cálculo y el tamaño de la salida. Claramente, una solución degenerada, aunque afortunadamente inadmisible a menos que P = NP) sería simplemente resolver el problema SAT y luego emitir un trivial 3 -SAT instancia ...)

EDITAR: según la respuesta de Ratchet, está claro ahora que la reducción a n-SAT es algo trivial (y que realmente debería haber pensado un poco más antes de publicar). Dejo esta pregunta abierta por un momento en caso de que alguien sepa la respuesta a la situación más general, de lo contrario, simplemente aceptaré la respuesta de Ratchet.

Cada cláusula SAT tiene 1, 2, 3 o más variables. La cláusula de 3 variables se puede copiar sin problemas

Las cláusulas variables 1 y 2 {a1}y {a1,a2}se pueden ampliar a {a1,a1,a1}y {a1,a2,a1}respectivamente.

La cláusula con más de 3 variables {a1,a2,a3,a4,a5}se puede expandir a {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}con s1y s2nuevas variables cuyo valor dependerá de qué variable en la cláusula original sea verdadera

Esto probablemente esté más allá del alcance de la pregunta, pero quería publicarlo de todos modos. Utilizando técnicas de complejidad parametrizada, se ha demostrado que, suponiendo que la jerarquía polinómica no se colapse a su tercer nivel, no existe un algoritmo de tiempo polinómico que tome una instancia de CNF-SAT en n variables con una longitud de cláusula ilimitada, y genera un instancia de k-CNF-SAT (sin cláusulas de longitud más que k) en n 'variables donde es polinomial en . Esto se desprende del trabajo de Fortnow y Santhanam , ver también el trabajo de seguimiento de Dell y van Melkebeek . En términos generales, el número de variables en la instancia de k-CNF-SAT siempre dependerá del número de cláusulas en su fórmula CNF-SAT.$n'$$n$

Si necesita una reducción de k-SAT a 3-SAT, la respuesta de trinquete funciona bien.

Si desea una reducción directa de la fórmula proposicional genérica a CNF (y a 3-SAT) entonces, al menos desde la "perspectiva de solucionadores SAT", creo que la respuesta a su pregunta ¿Cuál es la reducción 'más natural' ... ? , es: ¡ No hay reducción 'natural' !

De las conclusiones del Capítulo 2 - "Codificaciones CNF" del (muy bueno) libro: Manual de Satisfabilidad :

...
Por lo general, hay muchas formas de modelar un problema determinado en CNF, y se conocen pocas pautas para elegir entre ellas. A menudo hay una variedad de características del problema para modelar como variables, y algunas pueden pensar mucho en descubrirlas. Las codificaciones de tseitina son compactas y mecanizables, pero en la práctica no siempre conducen al mejor modelo, y algunas subformulas pueden expandirse mejor. Algunas cláusulas pueden omitirse por consideraciones de polaridad y pueden agregarse cláusulas implícitas de ruptura de simetría o bloqueadas. Las diferentes codificaciones pueden tener diferentes ventajas y desventajas, como el tamaño o la densidad de la solución, y lo que es una ventaja para un solucionador SAT puede ser una desventaja para otro. En resumen, el modelado CNF es un arte y a menudo debemos proceder por intuición y experimentación.
...

El algoritmo más conocido es el algoritmo Tseitin (G. Tseitin. Sobre la complejidad de la derivación en el cálculo proposicional. Automatización del razonamiento: documentos clásicos en lógica computacional, 2: 466–483, 1983. Springer-Verlag.)

Para una buena introducción a las codificaciones CNF, lea el libro sugerido Manual o Satisfabilidad . También puede leer algunos trabajos recientes y mirar las referencias; por ejemplo:

• P. Jackson y D. Sheridan. Conversiones de forma de cláusula para circuitos booleanos. En HH Hoos y DG Mitchell, editores, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004 , volumen 3542 de LNCS, páginas 183–198. Springer, 2004. (cuyo objetivo es reducir el número de cláusulas)
• P. Manolios, D. Vroon, Conversión de circuito eficiente a CNF. En Teoría y Aplicaciones de Pruebas de Satisfacción - SAT 2007 (2007), pp. 4-9

Permítanme publicar otra solución similar a la de Ratchel pero algo diferente. Esto está tomado directamente del capítulo 9 de la segunda edición del "Manual de diseño del algoritmo" de Steven Skiena

• Si la cláusula tiene un solo literal C = {z1}, cree dos nuevas variables v1 y v2 y cuatro nuevas cláusulas de 3 literales: {v1, v2, z1}, {! V1, v2, z1}, {v1,! v2, z1} y {! v1,! v2, z1}. Tenga en cuenta que la única forma en que las cuatro cláusulas pueden satisfacerse simultáneamente es si z1 = T, lo que también significa que se cumplirá la C original
• Si la cláusula tiene dos literales, C = {z1, z2}, cree una nueva variable v1 y dos nuevas cláusulas: {v1, z1, z2} y {! V1, z1, z2}. Nuevamente, la única manera de satisfacer ambas cláusulas es hacer que al menos una de z1 y z2 sea verdadera, satisfaciendo así C
• Si la cláusula tiene tres literales, C = {z1, z2, z3}, simplemente copie C en la instancia de 3-SAT sin cambios
• Si la cláusula tiene más de 3 literales C = {z1, z2, ..., zn}, cree n-3 nuevas variables y n-2 nuevas cláusulas en una cadena, donde para 2 <= j <= n-2 , Cij = {v1, j-1, zj + 1,! Vi, j}, Ci1 = {z1, z2,! Vi, 1} y Ci, n-2 = {vi, n-3, zn-1, zn}