Satisfatibilidade de Horn

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

Na lógica formal, Satisfatibilidade de Horn, ou HORNSAT, é o problema de decidir se um dado conjunto de cláusulas de Horn é satisfatível ou não.

Uma cláusula de Horn é uma cláusula com no máximo um literal positivo, chamado cabeça da cláusula, e qualquer número de literais negativos, formando o corpo da cláusula. Uma fórmula de Horn é uma fórmula proposicional formada pela conjunção de cláusulas de Horn. O problema da satisfatibilidade de Horn é solucionável em tempo linear. [1] Um algoritmo de tempo polinomial para satisfatibilidade de Horn é baseado na regra de propagação de unidade: se a fórmula contém uma cláusula composta de um único literal l (uma cláusula unitária), então todas as cláusulas que contenham l (exceto ela mesma) são removidas, e todas as cláusulas contendo \neg l tem esse literal removido. O resultado da segunda regra pode gerar uma outra cláusula unitária, a qual será propagada da mesma maneira. Se não existem cláusulas unitárias, a fórmula pode ser satisfeita simplesmente pela atribuição de valoração negativa às variáveis restantes. A fórmula é insatisfatível se essa transformação gera um par de cláusulas unitárias opostas l e \neg l . Satisfatibilidade de Horn é, na verdade, um dos problemas mais "difíceis" ou "mais expressivos" que se sabe ser computável em tempo polinomial, no sentido de que é um problema P-completo.[2]

Esse algoritmo também permite a determinação de uma valoração-verdade de formulas de Horn satisfatíveis: a todas as variáveis contidas em uma cláusula unitária é atribuído o valor que satisfaça a cláusula unitária em questão; a todos os outros literais é atribuída valoração negativa. A atribuição resultante é o modelo mínimo da fórmula de Horn, isto é, a atribuição ter um conjunto mínimo de variáveis cujo valor-verdade é positivo, onde a comparação é feita usando set containment.

Usar um algoritmo linear para propagação de unidade faz com que o algoritmo seja linear no tamanho da fórmula.

Uma generalização da classe das fórmulas de Horn é a das fórmulas renomeáveis de Horn (renameble-Horn formulae), que é o conjunto de fórmulas que podem ser passadas para a forma de Horn através da substituição de algumas variáveis por suas respectivas negações. Conferir a existência de tal substituição pode ser feito em tempo linear; portanto a satisfatibilidade de tais fórmulas está em P, já que pode ser solucionada realizando essa substituição e, em seguida, checando a satisfatibilidade da fórmula de Horn resultante.[3]

O problema da satisfatibilidade de Horn também pode ser requerido para lógica proposicional multi-valor (propositional many-valued logics). Os algoritmos não são geralmente lineares, mas alguns são polinomiais; ver Hähnle (2001 ou 2003) para uma pesquisa.[4] [5]

Referências[editar | editar código-fonte]

  1. Dowling, W., and Gallier, J., (1984) "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming, 3, 267-284
  2. Logical foundations of proof complexity. [S.l.]: Cambridge University Press, 2010. p. 224. ISBN 978-0-521-51729-4
  3. Chandru, Vijaya; Collette R. Coullard, Peter L. Hammer, Miguel Montañez, and Xiaorong Sun. (2005). "On renamable Horn and generalized Horn functions". Annals of Mathematics and Artificial Intelligence 1 (1–4): 33–47. DOI:10.1007/BF01531069.
  4. Reiner Hähnle. In: Dov M. Gabbay, Franz Günthner. Handbook of philosophical logic. 2nd ed. [S.l.]: Springer, 2001. p. 373. vol. 2. ISBN 978-0-7923-7126-7
  5. Reiner Hähnle. In: Melvin Fitting, Ewa Orlowska. Beyond two: theory and applications of multiple-valued logic. [S.l.]: Springer, 2003. ISBN 978-3-7908-1541-2

Ver Também[editar | editar código-fonte]

Ícone de esboço Este artigo sobre Informática é um esboço. Você pode ajudar a Wikipédia expandindo-o.