Único 1 en-3 SAT

Question

Supongamos que tengo una fórmula CNF con cláusulas de tamaño 2 y 3. Tiene una asignación satisfactoria única.

Sé el valor de cada bit de la asignación única porque se realizó a partir de un circuito de multiplicación binaria donde multiplicé dos números primos A y B de tal manera que A * B= S donde S es un número de semiprime. Añadí las condiciones que A!= 1, B!= 1 y A <= B, luego agregué el valor de S a la fórmula Asegúrese de que la asignación sea única. La única forma de satisfacer la fórmula es poner los valores de A y B en el orden correcto en los bits de entrada.

El número de literales verdaderos en cada cláusula es 1, 2 o 3. Porque conozco el valor de cada bit, puedo decir exactamente qué literales son verdaderos en cada cláusula, y cuídalos. Por ejemplo, sé qué cláusulas están satisfechas exactamente 1 literales. Y ese literal es lógicamente parte de la solución única.

Mi pregunta es simple: si elimino todas las cláusulas con más de 1 verdadero literal, ¿la asignación aún necesariamente será única?

En otras palabras, si quería anotar una prueba de resolución (probablemente exponencialmente larga) para demostrar que la solución es única (otro problema de la solución, en CO-NP), puedo escribirlo usando solo las cláusulas con 1 verdadero literal?

Intuitivamente, creo que sí, pero no puedo defender mi punto de vista, incluso cuando se piensa en el equivalente 2SAT.

Answer 1

Considere la siguiente CNF: $$ (A \ lor \ lnot b) \ Land (\ lNot A \ Lor B) \ Land (A \ Lor B). $$ Tiene una asignación satisfactoria única, $ a= b=top $ , que satisface la última cláusula dos veces.Sin embargo, si elimina la última cláusula, obtiene otra asignación satisfactoria, $ a= b=bot $ .