Traducción de SAT a HornSAT

26

¿Es posible traducir una fórmula booleana B en una conjunción equivalente de cláusulas Horn? El artículo de Wikipedia sobre HornSAT parece implicar que lo es, pero no he podido perseguir ninguna referencia.

Tenga en cuenta que no me refiero a "en tiempo polinómico", sino más bien "en absoluto".

reference-request lo.logic sat Evgenij Thorstensen
fuente

1

¿Qué quieres decir con "traducir"? Es obvio que hay instancias SAT que no se pueden escribir como una fórmula HornSAT. Por ejemplo, la cláusula (p o q). ¿Pero quizás quiere decir que desea una reducción tal que la fórmula SAT de entrada sea satisfactoria si la fórmula HornSAT de salida es satisfactoria? En ese caso, por supuesto, está la reducción de trivial, ya que no se preocupan por la eficiencia ...

arnab

No me refiero a equisatisfactable, ya que eso es realmente trivial sin restricciones de eficiencia. Me refiero a equivalente como en "tener las mismas asignaciones satisfactorias" cuando consideramos las variables comunes tanto a la instancia SAT como a la instancia HornSAT correspondiente (si tuviéramos que agregar algunas variables auxiliares, las proyectaremos). Estoy de acuerdo en que no debería ser posible, exactamente para el ejemplo (P v Q), pero no sé cómo demostrarlo. ¿Tienes un bosquejo de prueba en mente?

Evgenij Thorstensen

3

La pregunta sigue siendo ambigua. ¿Puedes explicar qué quieres decir con "proyectarlos"? ¿Quiere decir que "la asignación A satisface la instancia SAT F si hay una asignación B a variables auxiliares tales que (A, B) satisfaga la instancia HornSAT F '"? Si es así, creo que puedes hacerlo simplemente usando la integridad P de HornSAT.

Ryan Williams el

24

No. Las cláusulas de las conjunciones de Horn admiten menos modelos de Herbrand, que las disyunciones de los literales positivos no. Cf. Lloyd, 1987, Fundamentos de la programación lógica .

Los modelos de Herbrand menos tienen la propiedad de estar en las intersecciones de todos los satisfactores. Los modelos de Herbrand para son , que no contiene su intersección, por lo que, como dice arnab, es un ejemplo de fórmula que no se puede expresar como una conjunción de las cláusulas de Horn. $(a \lor b)$ $\{\{a\}, \{b\}, \{a,b\}\}$ $(a \lor b)$

Respuesta incorrecta sobrescrita

Charles Stewart
fuente

Inteligente, pero la cláusula -a_1 & ... & -a_n -> # no es una cláusula Horn.

Evgenij Thorstensen

@Evgenij: lo es.

Radu GRIGore

44

Una cláusula de trompeta es una disyunción de literales con a lo sumo un literal positivo. Traduciendo lo anterior a una disyunción de literales, obtenemos a_1 v ... v a_n, con todos los literales positivos. La cláusula anterior es dual-Horn, pero eso no ayuda a mi interés.

Evgenij Thorstensen

@rgrig: No, estaba confundido. @Evgenij: Respuesta corregida.

Charles Stewart

5

La capacidad de satisfacción se puede lograr de la siguiente manera (reducción de 2SAT a HornSAT). Entonces también se puede reducir a una fórmula Horn de esta manera. Gracias a Joshua Gorchow por señalar esta reducción. $(p \lor q)$

Entrada: una fórmula 2-SAT , con cláusulas , ..., en las variables , ..., . $\phi$ $C_1$ $C_k$ $x_1$ $x_n$

Construya una fórmula de bocina siguiente manera: $Q$

Habrá 4 ( elegir ) nuevas variables, una para cada posible $\times$ $n$ $2$ $+ 2n + 1$ cláusula 2-cnf posible en las variables con como máximo 2 literales ( no solo las cláusulas en ) - esto es incluyendo cláusulas de la unidad y la cláusula de vacío .. la nueva variable correspondiente a una cláusula de se denota por . $x$ $C_i$ $\phi$ $D$ $z_D$

El 4 ( elige ) proviene del hecho de que cada par de da lugar a cuatro cláusulas 2-cnf. El proviene del hecho de que cada $\times$ $n$ $2$ $(x_i, ~x_j)$ $2n$ $x_i$ puede crear cláusulas de 2 unidades. Y finalmente el "uno" proviene de la cláusula vacía. Entonces, el número total de posibles cláusulas 2-cnf es 4 ( elige ) . $=$ $\times$ $n$ $2$ $+ 2n + 1$

Si una cláusula 2-cnf sigue de otras dos cláusulas 2-cnf y en un solo paso de resolución, entonces agregamos la cláusula Horn a ... Nuevamente, hacemos esto para todos los posibles cláusulas 2-CNF - los 4 ( elegir ) de ellos - no sólo la . $F$ $D$ $E$ $(z_D \land z_E \to z_F)$ $Q$ $\times$ $n$ $2$ $+2n+1$ $C_i$

Luego agregamos las cláusulas unitarias a , para cada cláusula $z_{C_i}$ $Q$ $C_i$ aparece en la entrada de ... Por último, se añade la cláusula unidad a . $\phi$ $(\neg z_{empty})$ $Q$

La fórmula Cuerno ahora está completa. Observe que las variables utilizadas en son completamente diferentes de las utilizadas en . $Q$ $Q$ $\phi$

Martin Seymour
fuente

¿Alguien sabe de un algoritmo en la otra dirección? Dada una fórmula de Horn

, ¿existe un método para obtener una expresión equivalente 2SAT (2CNF)

, de modo que

sea satisfactoria si y solo si

ϕ_{1}

$\phi_1$

ϕ_{2}

$\phi_2$

ϕ_{1}

$\phi_1$

es? ¿Usando el mismo conjunto de variables, o usando variables adicionales, o usando un conjunto de variables completamente diferente (como se hizo en la respuesta anterior)? ¿O una prueba de que esto es imposible?

ϕ_{2}

$\phi_2$

Martin Seymour

2

No creo que sea posible. No hay forma, por ejemplo, de escribir como una conjunción de cláusulas de claxon ya que solo prohíbe una sola asignación de verdad, concretamente 0011. Cualquier cláusula de claxon con menos de 4 literales prohibirían más de 1 asignación de verdad, y las cláusulas de claxon con 4 literales solo pueden prohibir las asignaciones de verdad con un máximo de 0. $\phi = (X_1 \vee X_2 \vee \neg X_3 \vee \neg X_4)$ $\phi$

Editar: ¡Uy! No notaron que esto ya fue respondido

fuente

Traducción de SAT a HornSAT

Respuestas: