Verificar una sutileza de la prueba original de Karp de que SAT tiene una reducción de tiempo polinomial a 3SAT

8

En pocas palabras, mi pregunta es: ¿es la prueba original de Karp reducir SAT a 3SAT innecesariamente elaborada? Los detalles son los siguientes.

En su artículo de 1972 Reducibilidad entre problemas combinatorios , Karp demostró que SAT se reduce a 3SAT al afirmar:

Reemplace una cláusula , donde son literales , por donde es una nueva variable. Repita esta transformación hasta que ninguna cláusula tenga más de tres literales.σ1σ2...σmetroσyometro>3

(σ1σ2tu1)(σ3...σmetrotu¯1)(σ¯3tu1)...(σ¯metrotu1),
tu1

Me parece que las cláusulas finales (es decir, las cláusulas que contienen dos literales) aquí son innecesarias. Entonces, la construcción es correcta como está escrita pero es más elaborada de lo necesario. Sin las cláusulas de 2 literales, obtenemos la construcción que generalmente se da en los libros de texto de pregrado. ¿Es correcto o me falta algo obvio? Me siento extremadamente inseguro de mí mismo sugiriendo que cualquier cosa hecha por Karp podría expresarse con más elegancia.metro-2

John MacCormick
fuente

Respuestas:

9

La conjunción de las dos primeras cláusulas, es equisatisfactable a la cláusula original, como puede ser fácilmente marcado (cualquier valoración que satisfaga una de las también satisface una de las dos nuevas cláusulas, y puede extenderse a según sea necesario para satisfacer la otra; cualquier valoración que satisfaga ambas cláusulas nuevas debe satisfacer alguna , ya que no puede satisfacer ambas y .)(σ1σ2tu1)(σ3...σmetrotu¯1)σyotu1σyotu1tu¯1

Las cláusulas adicionales aseguran que sea, de hecho, equivalente a , pero hasta donde puedo ver, Karp en realidad no usa esto. Él acredita el artículo de Cook de 1971 por esta reducción particular, pero la versión que se encuentra allí (en realidad para las tautologías de DNF en lugar de la satisfacción de CNF) no presenta estas restricciones adicionales.tu1σ3...σmetro

Klaus Draeger
fuente
Gracias por la útil respuesta. Reformulando para amplificar y verificar mi comprensión, otra forma de afirmar esto es que las cláusulas adicionales aseguran que esto sea una reducción de #SAT a # 3SAT (ya que preservan el número de soluciones y no solo la existencia de soluciones).
John MacCormick