Satisfatibilidade de Horn
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 (uma cláusula unitária), então todas as cláusulas que contenham (exceto ela mesma) são removidas, e todas as cláusulas contendo 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 e . 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
- ↑ Dowling, William F.; Gallier, Jean H. (outubro de 1984). «Linear-time algorithms for testing the satisfiability of propositional horn formulae». The Journal of Logic Programming (em inglês) (3): 267–284. doi:10.1016/0743-1066(84)90014-1. Consultado em 30 de outubro de 2023
- ↑ Cook, Stephen; Nguyen, Phuong (2014). Logical foundations of proof complexity. Col: Perspectives in Logic. Cambridge University Press, Association for Symbolic Logic Paperback ed ed. New York: Cambridge University Press. ISBN 978-0-521-51729-4
- ↑ Chandru, Vijaya; Coullard, Collette R.; Hammer, Peter L.; Montañez, Miguel; Sun, Xiaorong (setembro de 1990). «On renamable Horn and generalized Horn functions». Annals of Mathematics and Artificial Intelligence (em inglês) (1-4): 33–47. ISSN 1012-2443. doi:10.1007/BF01531069. Consultado em 30 de outubro de 2023
- ↑ Reiner Hähnle (2001). «Advanced many-valued logics». In: Dov M. Gabbay, Franz Günthner. Handbook of philosophical logic. 2 2nd ed. [S.l.]: Springer. p. 373. ISBN 978-0-7923-7126-7
- ↑ Reiner Hähnle (2003). «Complexity of Many-valued Logics». In: Melvin Fitting, Ewa Orlowska. Beyond two: theory and applications of multiple-valued logic. [S.l.]: Springer. ISBN 978-3-7908-1541-2
