Mostrar código-fonte de Propagação de unidade

Propagação de Unidade (PU) ou a regra de um literal (RUL) é um [[procedimento]] de [[Prova automática de teoremas | prova automática de teoremas]] que pode simplificar um conjunto de [[Cláusula (lógica) | cláusulas]] (geralmente da [[Lógica proposicional | lógica proposicional]]).

==Definição==

O procedimento é baseado em cláusulas de unidade, ou seja, cláusulas que são compostas de um único [[Literal (lógica) | literal]]. Se um conjunto de cláusulas contém a cláusula de unidade <math>l</math>, as outras cláusulas são simplificadas pela aplicação das duas seguintes regras:
#toda cláusula contendo <math>l</math> é removido;
#em cada cláusula que contém <math>\neg l</math>  esse literal é excluído.
A aplicação destas duas regras conduz a um novo conjunto de cláusulas que é equivalente ao antigo. Por exemplo, o seguinte conjunto de cláusulas pode ser simplificado pela propagação de unidade porque contém a cláusula unidade <math>a</math>.
: <math>\{a \vee b, \neg a \vee c, \neg c \vee d, a\}</math>

Uma vez que <math>a \vee b</math> contém o literal <math>a</math>, esta cláusula pode ser removida completamente. Uma vez que  <math>\neg a \vee c</math> contém a negação da literal na cláusula de unidade, esse literal pode ser removido da cláusula. A cláusula de unidade a não é removida, o que tornaria o conjunto resultante não é equivalente ao original; esta cláusula pode ser removida se já armazenadas em alguma outra forma (ver secção "Utilizar um modelo parcial"). O efeito de propagação unidade pode ser resumido como se segue.
{| border="0" align="center" cellpadding="5" style="text-align: center;"
| <math>\{</math> || <math>a \vee b,</math> || <math>\neg a \vee c,</math> || <math>\neg c \vee d</math> || <math>a</math> || <math>\}</math>
|-
|   || (removido) || (<math>\neg a</math> deletado) || (sem alteração) || (sem alteração)
|-
| <math>\{</math> || &nbsp; || <math>c,</math> || <math>\neg c \vee d,</math> || <math>a</math> || <math>\}</math>
|}
O conjunto resultante de cláusulas <math>\{c, \neg c \vee d, a\}</math> é equivalente ao de cima. A nova cláusula de unidade <math>c</math> que resulta da propagação de unidade pode ser usada para uma aplicação posterior da propagação de unidade, o que transformaria <math>\neg c \vee d</math> em <math>d</math>.

==Propagação de unidade e resolução==

A segunda regra da propagação de unidade pode ser visto como uma forma restrita do [[Princípio da resolução | princípio da resolução]], em que um dos dois resolvidos deve ser sempre uma cláusula de unidade. Quanto à resolução, a propagação de unidade é uma regra de inferência correta, em que nunca produz uma nova cláusula que não foi vinculada pelos antigos. A diferença entre a propagação unidade e resolução são:
resolução é um procedimento de refutação completa enquanto a propagação da unidade não é, em outras palavras, mesmo se um conjunto de cláusula é contraditória, a propagação de unidade pode não gerar uma inconsistência;
as duas cláusulas que são resolvidas não podem, em geral, ser removidas após a cláusula gerada ser adicionada ao conjunto; pelo contrário, a cláusula de unidade não envolvida em uma propagação de unidade pode ser removida, quando a sua simplificação é adicionada ao conjunto;
resolução em geral não inclui a primeira regra utilizada na propagação de unidade.
Resolução cálculos que incluem subsunção pode modelar a regra um por subsunção e a regra dois por uma etapa de resolução de unidade, seguido de subsunção.
Propagação de unidade, aplicada, repetidamente, à medida que novas cláusulas de unidades são geradas, é um algoritmo de satisfatibilidade completa para conjuntos de [[Cláusula de Horn | cláusulas de Horn]] proposicionais; mas também  gera um modelo mínimo para o conjunto se satisfeito: ver satisfatibilidade de Horn.

==Usando um modelo parcial==

As cláusulas unitárias que estão presentes em um conjunto de cláusulas ou podem  ser derivadas a partir dele podem ser armazenadas na forma de um modelo parcial (este modelo parcial pode também conter outros literais, dependendo da aplicação). Neste caso, a propagação de unidade é realizada com base nos literais do modelo parcial, e as cláusulas unitárias são removidas se o seu literal está no modelo. No exemplo acima, a cláusula de unidade <math>a</math> seria adicionada ao modelo parcial; a simplificação do conjunto de cláusula seria então proceder como acima, com a diferença de que a cláusula de unidade <math>a</math> é agora removida do conjunto. O conjunto resultante de cláusula é equivalente ao original sob o pressuposto de validade dos literais no modelo parcial.

==Complexidade==

A aplicação direta da propagação de unidade leva [[Ordem quadrática | tempo quadrático]] no tamanho total do conjunto para se verificar. Que é definida como sendo a soma do tamanho de todas as cláusulas, onde o tamanho de cada cláusula é o número de literais que ele contém.
A propagação de unidade pode, contudo, ser feita em tempo linear, armazenando, para cada variável, a lista de cláusulas em que cada literal está contido. Por exemplo, o conjunto acima pode ser representado enumerando cada cláusula como se segue:
: <math>\{1: a \vee b, 2: \neg a \vee c, 3: \neg c \vee d, 4: a\}</math>
e, em seguida, armazenar, para cada variável, a lista de cláusulas que contêm a variável ou sua negação:

: <math>a : 1\ 2\ 4</math>

: <math>b : 1\,</math>

: <math>c : 2\ 3</math>

: <math>d : 3\, </math>

Esta estrutura de dados simples pode ser construída em tempo linear no tamanho do conjunto, e permite encontrar todas as cláusulas que contenham uma variável muito facilmente. Propagação de unidade de um literal pode ser realizada de forma eficiente, verificando apenas a lista de cláusulas que contenham a variável do literal. Mais precisamente, o tempo total de execução para fazer a propagação de unidade para todas as cláusulas de unidade é linear no tamanho do conjunto de cláusulas.

==Veja também==
*[[Cláusula de Horn]]
*[[Prova automática de teoremas]]
*[[Algoritmo DPLL]]

==Referências==
* W. Dowling and J. Gallier (1984). Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1(3):267–284.
* H. Zhang and M. Stickel (1996). An efficient algorithm for unit-propagation. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics.

[[Categoria:Lógica matemática]]