La propagación unitaria ( UP ) o la propagación de restricción booleana ( BCP ) o la regla de un literal ( OLR ) es un procedimiento de prueba automatizada de teoremas que puede simplificar un conjunto de cláusulas (generalmente proposicionales ) .
Definición
El procedimiento se basa en cláusulas unitarias , es decir, cláusulas que se componen de un solo literal . Debido a que cada cláusula debe cumplirse, sabemos que este literal debe ser verdadero. Si un conjunto de cláusulas contiene la cláusula unitaria, las demás cláusulas se simplifican mediante la aplicación de las dos reglas siguientes:
- cada cláusula (que no sea la cláusula unitaria en sí) que contiene se elimina (la cláusula se cumple si es);
- en cada cláusula que contiene este literal es eliminado ( no puede contribuir a que quede satisfecho).
La aplicación de estas dos reglas conduce a un nuevo conjunto de cláusulas que es equivalente al anterior.
Por ejemplo, el siguiente conjunto de cláusulas se puede simplificar mediante la propagación unitaria porque contiene la cláusula unitaria .
Desde contiene el literal , esta cláusula se puede eliminar por completo. Desdecontiene la negación del literal en la cláusula unit, este literal se puede eliminar de la cláusula. La cláusula de unidadno se elimina; esto haría que el conjunto resultante no sea equivalente al original; esta cláusula puede eliminarse si ya está almacenada en alguna otra forma (consulte la sección "Uso de un modelo parcial"). El efecto de la propagación unitaria se puede resumir de la siguiente manera.
(remoto) | ( eliminado) | (sin alterar) | (sin alterar) | ||
El conjunto de cláusulas resultante es equivalente al anterior. La nueva cláusula unitaria que resulta de la unidad de propagación se puede utilizar para una aplicación adicional de la unidad de propagación, que transformaría dentro .
Propagación y resolución de la unidad
La segunda regla de propagación unitaria puede verse como una forma restringida de resolución , en la que uno de los dos resolutivos debe ser siempre una cláusula unitaria. En cuanto a la resolución, la propagación de unidades es una regla de inferencia correcta, en el sentido de que nunca produce una nueva cláusula que no estuviera implícita en las anteriores. Las diferencias entre la propagación y la resolución de la unidad son:
- la resolución es un procedimiento de refutación completo, mientras que la propagación unitaria no lo es; en otras palabras, incluso si un conjunto de cláusulas es contradictorio, es posible que la propagación de unidades no genere una inconsistencia;
- en general, las dos cláusulas que se resuelven no se pueden eliminar después de agregar la cláusula generada al conjunto; por el contrario, la cláusula no unitaria involucrada en una propagación unitaria puede eliminarse cuando se agrega su simplificación al conjunto;
- En general, la resolución no incluye la primera regla utilizada en la propagación unitaria.
Los cálculos de resolución que incluyen la subsunción pueden modelar la regla uno por subsunción y la regla dos por un paso de resolución unitario, seguido de la subsunción.
La propagación unitaria, que se aplica repetidamente a medida que se generan nuevas cláusulas unitarias, es un algoritmo de satisfacibilidad completo para conjuntos de cláusulas Horn proposicionales ; también genera un modelo mínimo para el conjunto si es satisfactorio: ver Satisfacción de Horn .
Usando un modelo parcial
Las cláusulas unitarias que están presentes en un conjunto de cláusulas o que se pueden derivar de él se pueden almacenar en forma de modelo parcial (este modelo parcial también puede contener otros literales, dependiendo de la aplicación). En este caso, la propagación de unidades se realiza en función de los literales del modelo parcial y las cláusulas de unidad se eliminan si su literal está en el modelo. En el ejemplo anterior, la cláusula unitariase agregaría al modelo parcial; la simplificación del conjunto de cláusulas procedería entonces como arriba con la diferencia de que la cláusula unitariaahora se elimina del conjunto. El conjunto de cláusulas resultante es equivalente al original bajo el supuesto de validez de los literales en el modelo parcial.
Complejidad
La implementación directa de la propagación de unidades lleva tiempo cuadrático en el tamaño total del conjunto a verificar, que se define como la suma del tamaño de todas las cláusulas, donde el tamaño de cada cláusula es el número de literales que contiene.
Sin embargo, la propagación de unidades se puede hacer en tiempo lineal almacenando, para cada variable, la lista de cláusulas en las que está contenido cada literal. Por ejemplo, el conjunto anterior se puede representar numerando cada cláusula de la siguiente manera:
y luego almacenar, para cada variable, la lista de cláusulas que contienen la variable o su negación:
Esta estructura de datos simple se puede construir en el tiempo de forma lineal en el tamaño del conjunto, y permite encontrar todas las cláusulas que contienen una variable con mucha facilidad. La propagación unitaria de un literal se puede realizar de manera eficiente escaneando solo la lista de cláusulas que contienen la variable del literal. Más precisamente, el tiempo de ejecución total para hacer la propagación unitaria para todas las cláusulas unitarias es lineal en el tamaño del conjunto de cláusulas.
Ver también
Referencias
- Dowling, William F .; Gallier, Jean H. (1984), "Algoritmos de tiempo lineal para probar la satisfacibilidad de las fórmulas proposicionales de Horn", Journal of Logic Programming , 1 (3): 267-284, doi : 10.1016 / 0743-1066 (84) 90014- 1 , MR 0770156.
- H. Zhang y M. Stickel (1996). Un algoritmo eficiente para la propagación de unidades. En Actas del Cuarto Simposio Internacional sobre Inteligencia Artificial y Matemáticas .