La propagación unitaria ( UP ) o propagación de restricción booleana ( BCP ) o la regla de un literal ( OLR ) es un procedimiento de demostración automática de teoremas que puede simplificar un conjunto de cláusulas (generalmente proposicionales ) .
El procedimiento se basa en cláusulas unitarias , es decir, cláusulas que están compuestas por un único literal , en forma normal conjuntiva . Como 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:
La aplicación de estas dos reglas da lugar a un nuevo conjunto de cláusulas que es equivalente al antiguo.
Por ejemplo, el siguiente conjunto de cláusulas se puede simplificar mediante propagación de unidades porque contiene la cláusula de unidad .
Dado que contiene el literal , esta cláusula se puede eliminar por completo. Dado que contiene la negación del literal en la cláusula de unidad, este literal se puede eliminar de la cláusula. La cláusula de unidad no se elimina; esto haría que el conjunto resultante no sea equivalente al original; esta cláusula se puede eliminar si ya está almacenada en alguna otra forma (consulte la sección "Uso de un modelo parcial"). El efecto de la propagación de unidades se puede resumir de la siguiente manera.
El conjunto de cláusulas resultante es equivalente al anterior. La nueva cláusula de unidad que resulta de la propagación de unidades se puede utilizar para una aplicación posterior de la propagación de unidades, que se transformaría en .
La segunda regla de propagación de unidades puede verse como una forma restringida de resolución , en la que uno de los dos resolutores debe ser siempre una cláusula de unidad. 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 esté implícita en las anteriores. Las diferencias entre la propagación de unidades y la resolución son:
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 de unidades, aplicada repetidamente a medida que se generan nuevas cláusulas de unidad, es un algoritmo de satisfacibilidad completo para conjuntos de cláusulas de Horn proposicionales ; también genera un modelo mínimo para el conjunto si es satisfacible: consulte satisfacibilidad de Horn .
Las cláusulas unitarias que están presentes en un conjunto de cláusulas o que pueden derivarse de él pueden almacenarse en forma de un modelo parcial (este modelo parcial también puede contener otros literales, según 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 unitarias se eliminan si su literal está en el modelo. En el ejemplo anterior, la cláusula unitaria se añadiría al modelo parcial; la simplificación del conjunto de cláusulas se llevaría a cabo como se ha indicado anteriormente, con la diferencia de que ahora la cláusula unitaria 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.
La implementación directa de la propagación de unidades toma un 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 realizar en tiempo lineal almacenando, para cada variable, la lista de cláusulas en las que se encuentra 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 sencilla estructura de datos se puede construir en un tiempo lineal en relación con 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 total de ejecución para realizar la propagación unitaria de todas las cláusulas unitarias es lineal en relación con el tamaño del conjunto de cláusulas.
