¿Cómo demostrar que una versión restringida de 3SAT en la que no literal puede ocurrir más de una vez, es resoluble en tiempo polinómico?

Question

Estoy tratando de averiguar una asignación (tomado del libro Algoritmos - por S. Dasgupta, CH Papadimitriou, y Vazirani UV , capítulo 8, el problema 8.6a), y estoy parafraseando lo que dice:

Dado que 3SAT sigue siendo NP-completo incluso cuando restringido a fórmulas en las que Cada uno aparece literales a lo sumo dos veces, muestran que si aparece cada vez más literales a, entonces el problema es resoluble en tiempo polinómico.

he tratado de resolver este separando las cláusulas en varios grupos:

1. Las cláusulas que no tenían ninguna variable en común con el resto de las cláusulas
2. cláusulas que sólo tenían 1 variable en común
3. cláusulas que tenía 2 variables en común
4. Las cláusulas que tenían las 3 variables en común

Mi razonamiento se intentó a lo largo de las líneas que el # de tales grupos es finito (debido a la restricción impuesta de ningún ser literal más de una vez está presente), y que se podía tratar de satisfacer el grupo más restringido primera (grupo 4) y a continuación, sustituir el resultado en los grupos de menor restringidos (3, 2 y 1), pero me di cuenta de que esto no fue bastante conseguirme en cualquier lugar, ya que esto no se diferencia mucho del caso para la versión restringida de 3SAT en el que cada literal puede aparecer como máximo dos veces, que se ha demostrado que es NP-completo.

He intentado buscar en línea para cualquier pista / soluciones, pero todo lo que podía conseguir era el este enlace, en el que se indique la indirecta no tenía sentido suficiente para mí, que yo estoy aquí que reproduce literalmente:

Sugerencia: Dado que cada una aparece literales a lo sumo una vez, convertir este problema a otro 2SAT - tiempo, por lo tanto polinomio, si un literal $ x_i $ aparece en la cláusula $ C_J $ y se complementan de $ x_i $ (es decir, $ \ overline {x_i } $) en la cláusula $ $ C_K, construir una nueva cláusula cláusula $ C_J \ lor \ overline {C_K} $.

Tanto C_J $ $ y $ $ C_K tener tres literales cada uno - Yo no entiendo cómo debería ir sobre su conversión en 2SAT haciendo $ C_J \ lor \ overline {C_K} $ (o $ \ overline {C_J \ lor C_K} $ si leo de forma incorrecta).

Cualquier ayuda, ya sea en el descifrado de la pista, o proporcionando un camino puedo explorar sería muy apreciada.

Answer 1

Sin pérdida de generalidad, podemos suponer que cada variable aparece exactamente una vez positiva y negativa exactamente una vez (si es una variable sólo aparece una vez establecido su valor para satisfacer la cláusula y eliminar la cláusula). También podemos suponer que una variable no aparece en una cláusula más de una vez (si es una variable aparece tanto positiva como negativamente en una cláusula, a continuación, la cláusula se satisface y se puede quitar). Estos no alterarán la satisfacibilidad.

Ahora utilice el regla de resolución para eliminar las variables una por una (ya cada variable aparece exactamente una vez positiva y negativa, una vez este es un proceso determinista). Si en algún momento se obtiene la cláusula vacía el conjunto de cláusulas es insaciable, de lo contrario es satisfiable. Esto se debe a:

• resolución es un sistema de prueba proposicional completa (es decir, si una cláusula es lógicamente implicado por el conjunto de cláusulas entonces es derivable del conjunto de cláusulas usando sólo la regla de resolución),

• un conjunto de cláusulas es unsatisfiable si y sólo si es lógicamente implica la cláusula vacía.

Este algoritmo tomará tiempo polinomio dado que cada variable se resuelve exactamente una vez. En particular, cada aplicación de la resolución se reducirá el número total de cláusulas por uno, por lo que el número de cláusulas no aumenta. Por ejemplo, la aplicación de la resolución a $ (x \ lor B) \ tierra (\ overline {x} \ lor C) \ tierra \ dots) $ rendimientos $ (B \ lor C) \ tierra \ dots $, que tiene una cláusula menos que antes resolución. Por el contrario, si aplicó esta a una fórmula 3SAT con ninguna restricción en el número de apariciones de cada literal, la aplicación de la resolución podría hacer que el número de cláusulas de aumentar exponencialmente.