Traduzindo SAT para HornSAT

26

É possível traduzir uma fórmula booleana B em uma conjunção equivalente de cláusulas de Horn? O artigo da Wikipedia sobre HornSAT parece sugerir que sim, mas não pude buscar nenhuma referência.

Note que eu não quero dizer "em tempo polinomial", mas sim "em tudo".

reference-request lo.logic sat Evgenij Thorstensen
fonte

1

O que você quer dizer com "traduzir"? É óbvio que existem instâncias SAT que não podem ser escritas como uma fórmula HornSAT. Por exemplo, a cláusula (p ou q). Mas talvez você queira dizer uma redução tal que a fórmula SAT de entrada seja satisfatória se a fórmula HornSAT de saída for satisfatória? Nesse caso, é claro, há a redução trivial desde que você não se importa com eficiência ...

arnab

Não estou falando de insatisfatório, pois isso é de fato trivial sem restrições à eficiência. Quero dizer equivalente como em "tem as mesmas atribuições satisfatórias" quando consideramos as variáveis comuns à instância SAT e à instância HornSAT correspondente (se tivermos que adicionar algumas variáveis auxiliares, as projetamos). Concordo que não deveria ser possível, exatamente para o exemplo (P v Q), mas não sei como provar. Você tem um esboço de prova em mente?

Evgenij Thorstensen

3

A questão ainda é ambígua. Você pode explicar o que você quer dizer com "projetá-los"? Você quer dizer "a atribuição A satisfaz a instância SAT F se houver uma atribuição B para variáveis auxiliares tais que (A, B) satisfaça a instância F 'do HornSAT"? Nesse caso, acho que você pode fazê-lo simplesmente usando a completude P do HornSAT.

Ryan Williams

24

Não. As cláusulas de conjunções de Horn admitem menos modelos de Herbrand, o que não ocorre com disjunções de literais positivos. Cf. Lloyd, 1987, Fundamentos da Programação Lógica .

Os modelos menos Herbrand têm a propriedade de que estão nas interseções de todos os satisfadores. Os modelos de Herbrand para são , que não contêm sua interseção, portanto, como diz arnab, é um exemplo de fórmula que não pode ser expresso como uma conjunção de cláusulas de Horn. $(a \lor b)$ $\{\{a\}, \{b\}, \{a,b\}\}$ $(a \lor b)$

Resposta incorreta substituída

Charles Stewart
fonte

Inteligente, mas a cláusula -a_1 & ... & -a_n -> # não é uma cláusula Horn.

Evgenij Thorstensen

@ Evgenij: É.

Radu GRIGore 18/08/10

4

Uma cláusula de corneta é uma disjunção de literais com no máximo um literal positivo. Traduzindo o exposto acima para uma disjunção de literais, obtemos a_1 v ... v a_n, com todos os literais positivos. A cláusula acima é buzina dupla, mas isso não ajuda no meu interesse.

Evgenij Thorstensen

@rgrig: Não, eu estava confuso. @ Evgenij: Resposta corrigida.

Charles Stewart

5

A equivalência pode ser alcançada da seguinte maneira (redução de 2SAT para HornSAT). Portanto também pode ser reduzido a uma fórmula de Horn dessa maneira. Agradecemos a Joshua Gorchow por apontar essa redução. $(p \lor q)$

Entrada: Uma fórmula 2-SAT , com cláusulas , ..., nas variáveis , ..., . $\phi$ $C_1$ $C_k$ $x_1$ $x_n$

Construa uma fórmula chifre da seguinte maneira: $Q$

Haverá 4 ( $\times$ $n$ escolha ) novas variáveis, uma para cada possível cláusula 2-cnf possível nas variáveis com no máximo 2 literais ( não apenas as cláusulas em ) - isso é incluindo cláusulas unitários e a cláusula vazio .. a nova variável que corresponde a uma cláusula será denotado por . $2$ $+ 2n + 1$ $x$ $C_i$ $\phi$ $D$ $z_D$

O 4 ( escolha ) vem do fato de que cada par de $\times$ $n$ $2$ gera quatro cláusulas 2-cnf. O vem do fato de que cada pode criar 2 cláusulas de unidade. E finalmente o "one" vem da cláusula vazia. Portanto, o número total de cláusulas 2-cnf possíveis é 4 ( escolha ) . $(x_i, ~x_j)$ $2n$ $x_i$ $=$ $\times$ $n$ $2$ $+ 2n + 1$

Se uma cláusula 2-cnf segue de duas outras cláusulas 2-cnf e em uma única etapa de resolução, adicionamos a cláusula Horn $F$ $D$ $E$ a ... Novamente, fazemos isso para todas as possíveis cláusulas 2-cnf - todas as 4 ( escolha ) delas - não apenasa . $(z_D \land z_E \to z_F)$ $Q$ $\times$ $n$ $2$ $+2n+1$ $C_i$

Em seguida, adicionamos as cláusulas unitárias a, para cada cláusula aparecendo na entrada... Por fim, adicionar o cláusula unidadepara. $z_{C_i}$ $Q$ $C_i$ $\phi$ $(\neg z_{empty})$ $Q$

A fórmula Horn está agora completa. Observe que as variáveis usadas em são completamente diferentes das usadas em . $Q$ $Q$ $\phi$

Martin Seymour
fonte

Alguém está ciente de um algoritmo na outra direção? Dada uma fórmula de Horn

, existe um método para obter uma expressão 2SAT (2CNF) equivalente

ϕ_{1}

$\phi_1$

, de modo que

seja satisfatório se e somente se

for? Usando o mesmo conjunto de variáveis, ou usando variáveis extras, ou usando um conjunto completamente diferente de variáveis (como feito na resposta acima)? Ou uma prova de que isso é impossível?

ϕ_{2}

$\phi_2$

ϕ_{1}

$\phi_1$

ϕ_{2}

$\phi_2$

Martin Seymour

2

Eu não acho que é possível. Não há nenhuma maneira, por exemplo, para escrever como um conjunto de cláusulas do corno desde somente os criminosos uma única atribuição verdade, a saber, 0011. Qualquer cláusula chifre com menos de 4 literais proibiriam mais de 1 atribuição de verdade, e cláusulas de corneta com 4 literais só podem proibir atribuições de verdade com no máximo um 0. $\phi = (X_1 \vee X_2 \vee \neg X_3 \vee \neg X_4)$ $\phi$

Edit: oops não percebeu isso já foi respondido

fonte

Traduzindo SAT para HornSAT

Respostas: