Comment convertir une clause CNF en forme de cor en utilisant Prolog? J'essaye de créer un solveur de SAT qui a le CNF comme entrée, qui sera besoin de convertir en forme de corne.Conversion en forme de klaxon à partir de CNF
Les clauses de cor sont un sous-ensemble de CNF. A savoir CNF peut être considérée comme conjonction de clauses générales, où chaque clause a la forme suivante et où Ai, Bk sont des variables propositionnelles et n> = 0 et m> = 0:
A1 v .. v An v ~B1 v .. v ~Bm
Ai sont les littéraux positifs et les ~ Bk sont les littéraux négatifs. clauses de Horn sont maintenant les clauses générales qui ont au maximum un littéral positif, soit n = < 1. A savoir qui sont soit de la forme comme suit:
A1 v ~B1 v .. v ~Bm
~B1 v .. v ~Bm
Maintenant, il est impossible de convertir tous les CNF en clauses de Horn, même si nous permettons de changer le signe d'un littéral dans la représentation. Prenez cette formule Nae (A, B, C) = (A XOR B) v (B XOR C) et le signe correspondant changeant des variantes comme CNF:
nae(A,B,C) = (~A v ~B v ~C) & (A v B v C)
nae(A,B,~C) = (~A v ~B v C) & (A v B v ~C)
nae(A,~B,C) = (~A v B v ~C) & (A v ~B v C)
nae(A,~B,~C) = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,C) = (~A v B v C) & (A v ~B v ~C)
nae(~A,B,~C) = (~A v B v ~C) & (A v ~B v C)
nae(~A,~B,C) = (~A v ~B v C) & (A v B v ~C)
nae(~A,~B,~C) = (~A v ~B v ~C) & (A v B v C)
Ils sont toutes les clauses non-Horn donc une traduction de changement de nom n'est pas possible. Mais peut-être utiliser d'autres réductions, éventuellement non polynomiales, peuvent être utilisées pour traduire CNF en clauses de corne.
P.S .: L'exemple nae (A, B, C) est tiré de here.
Cela peut être utile si vous avez défini la forme de l'avertisseur et sa différence par rapport au format CNF que vous utilisez, car le protocole CNF peut être utilisé pour coder les formules d'avertisseur. –
Cela n'a pas beaucoup de sens à mon sens. Etre très informel: résoudre CNF est NP-difficile, résoudre HornSat est dans P. Cela signifie (en utilisant des arguments de base par contradiction): complexité-sage, cette transformation est aussi difficile que la résolution de l'original CNF-SAT (NP-hard) et la sortie peut être de taille exponentielle (pas grand chose que vous pouvez faire avec votre solveur HornSAT)! – sascha
Kyle Jones, comment CNF peut-il être utilisé pour encoder des formules Horn? –