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]