Propagação de unidade

Propagação de Unidade (PU) ou a regra de um literal (RUL) é um procedimento de prova automática de teoremas que pode simplificar um conjunto de cláusulas (geralmente da 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. Se um conjunto de cláusulas contém a cláusula de unidade $l$, as outras cláusulas são simplificadas pela aplicação das duas seguintes regras:

1. toda cláusula contendo $l$ é removido;
2. em cada cláusula que contém $\neg l$ 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 $a$.

$\{a\vee b,\neg a\vee c,\neg c\vee d,a\}$

Uma vez que $a\vee b$ contém o literal $a$, esta cláusula pode ser removida completamente. Uma vez que $\neg a\vee c$ 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.

$\{$	$a\vee b,$	$\neg a\vee c,$	$\neg c\vee d$	$a$	$\}$
	(removido)	($\neg a$ deletado)	(sem alteração)	(sem alteração)
$\{$		$c,$	$\neg c\vee d,$	$a$	$\}$

O conjunto resultante de cláusulas $\{c,\neg c\vee d,a\}$ é equivalente ao de cima. A nova cláusula de unidade $c$ que resulta da propagação de unidade pode ser usada para uma aplicação posterior da propagação de unidade, o que transformaria $\neg c\vee d$ em $d$.

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, 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á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 $a$ 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 $a$ é 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 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:

$\{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}$

e, em seguida, armazenar, para cada variável, a lista de cláusulas que contêm a variável ou sua negação:

$a:1\ 2\ 4$

$b:1\,$

$c:2\ 3$

$d:3\,$

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.