Traduction de SAT en HornSAT

26

Est-il possible de traduire une formule booléenne B en une conjonction équivalente de clauses Horn? L'article de Wikipédia sur HornSAT semble impliquer que c'est le cas, mais je n'ai pu chasser aucune référence.

Notez que je ne veux pas dire "en temps polynomial", mais plutôt "du tout".

reference-request lo.logic sat Evgenij Thorstensen
la source

1

Qu'entendez-vous par «traduire»? Il est évident qu'il existe des instances SAT qui ne peuvent pas être écrites en tant que formule HornSAT. Par exemple, la clause (p ou q). Mais peut-être voulez-vous dire que vous voulez une réduction telle que la formule SAT d'entrée soit satisfiable si la formule HornSAT de sortie est satisfiable? Dans ce cas, bien sûr, il y a la réduction triviale puisque vous ne vous souciez pas de l'efficacité ...

arnab

Je ne veux pas dire équisatisfiable, car c'est en effet trivial sans restrictions d'efficacité. Je veux dire équivalent comme dans «avoir les mêmes affectations satisfaisantes» lorsque nous considérons les variables communes à la fois à l'instance SAT et à l'instance HornSAT correspondante (si nous devions ajouter des variables auxiliaires, nous les projetons). Je suis d'accord que cela ne devrait pas être possible, exactement pour l'exemple (P v Q), mais je ne sais pas comment le prouver. Avez-vous un croquis de preuve en tête?

Evgenij Thorstensen

3

La question est toujours ambiguë. Pouvez-vous expliquer ce que vous entendez par «les projeter»? Voulez-vous dire que "l'affectation A satisfait l'instance SAT F s'il existe une affectation B aux variables auxiliaires telle que (A, B) satisfait l'instance F HornSAT"? Si oui, alors je pense que vous pouvez le faire en utilisant simplement la P-complétude de HornSAT.

Ryan Williams

24

Non. Les conjonctions de clauses de Horn admettent le moins les modèles de Herbrand, contrairement aux disjonctions de littéraux positifs. Cf. Lloyd, 1987, Fondements de la programmation logique .

Les modèles de moindre Herbrand ont la propriété d'être dans les intersections de tous les satisfaits. Les modèles Herbrand pour sont , qui ne contient pas son intersection, comme le dit arnab, est un exemple de formule qui ne peut pas être exprimée comme une conjonction de clauses Horn. $(a \lor b)$ $\{\{a\}, \{b\}, \{a,b\}\}$ $(a \lor b)$

Réponse incorrecte remplacée

Charles Stewart
la source

Intelligent, mais la clause -a_1 & ... & -a_n -> # n'est pas une clause Horn.

Evgenij Thorstensen

@Evgenij: Oui.

Radu GRIGore

4

Une clause cor est une disjonction de littéraux avec au plus un littéral positif. En traduisant ce qui précède en une disjonction de littéraux, nous obtenons a_1 v ... v a_n, tous les littéraux étant positifs. La clause ci-dessus est à double corne, mais cela n'aide pas mon intérêt.

Evgenij Thorstensen

@rgrig: Non, j'étais confus. @Evgenij: réponse fixe.

Charles Stewart

5

L'exquiabilité peut être obtenue de la manière suivante (réduction de 2SAT à HornSAT). Ainsi peut également être réduit à une formule de Horn de cette manière. Merci à Joshua Gorchow d'avoir signalé cette réduction. $(p \lor q)$

Entrée: Une formule 2-SAT , avec les clauses , ..., sur les variables , ..., . $\phi$ $C_1$ $C_k$ $x_1$ $x_n$

Construisez une formule de klaxon comme suit: $Q$

Il y aura 4 ( choisir ) nouvelles variables, une pour chaque clause 2-cnf possible sur les variables avec au plus 2 littéraux ( pas seulement les clauses dans ) - c'est y compris les articles de l' unité et la clause vide .. la nouvelle variable correspondant à une clause sera désigné par . $\times$ $n$ $2$ $+ 2n + 1$ $x$ $C_i$ $\phi$ $D$ $z_D$

Le 4 ( choisir ) vient du fait que chaque paire de donne lieu à quatre clauses 2-cnf. Le vient du fait que chaque peut créer 2 clauses unitaires. Et enfin le "un" vient de la clause vide. Donc le nombre total de clauses 2-cnf possibles est 4 ( choisissez ) . $\times$ $n$ $2$ $(x_i, ~x_j)$ $2n$ $x_i$ $=$ $\times$ $n$ $2$ $+ 2n + 1$

Si une clause 2-cnf découle de deux autres clauses 2-cnf et par une seule étape de résolution, alors nous ajoutons la clause Horn à ... Encore une fois, nous le faisons pour toutes les clauses 2-cnf possibles - toutes les 4 ( choisir ) d'entre elles - pas seulement le . $F$ $D$ $E$ $(z_D \land z_E \to z_F)$ $Q$ $\times$ $n$ $2$ $+2n+1$ $C_i$

Ensuite , nous ajoutons les clauses de l' unité à , pour chaque clause apparaissant dans l'entrée ... Enfin, nous ajoutons la clause unitaire à . $z_{C_i}$ $Q$ $C_i$ $\phi$ $(\neg z_{empty})$ $Q$

La formule Horn est maintenant terminée. Observez que les variables utilisées dans sont complètement différentes de celles utilisées dans . $Q$ $Q$ $\phi$

Martin Seymour
la source

Quelqu'un connaît-il un algorithme dans l'autre sens? Étant donné une formule de Horn

, existe-t-il une méthode pour obtenir une expression 2SAT (2CNF) équivalente

, de sorte que

soit satisfaisable si et seulement si

est? En utilisant le même ensemble de variables, ou en utilisant des variables supplémentaires, ou en utilisant un ensemble de variables complètement différent (comme cela est fait dans la réponse ci-dessus)? Ou une preuve que c'est impossible?

ϕ_{1}

$\phi_1$

ϕ_{2}

$\phi_2$

ϕ_{1}

$\phi_1$

ϕ_{2}

$\phi_2$

Martin Seymour

2

Je ne pense pas que ce soit possible. Il n'y a aucun moyen, par exemple, d'écrire tant que conjonction de clauses de cor puisque interdit uniquement une seule affectation de vérité, à savoir 0011. Toute clause de cor avec moins de 4 littéraux interdiraient plus d'une affectation de vérité, et les clauses de cor avec 4 littéraux ne peuvent interdire que les affectations de vérité avec au plus un 0. $\phi = (X_1 \vee X_2 \vee \neg X_3 \vee \neg X_4)$ $\phi$

Edit: oops n'a pas remarqué que cette réponse a déjà été répondue

la source

Traduction de SAT en HornSAT

Réponses: