stringtranslate.com

Propagación de unidades

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 ) .

Definición

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:

  1. se elimina cada cláusula (excepto la cláusula unitaria misma) que contenga (la cláusula se cumple si es);
  2. en cada cláusula que contiene este literal se elimina ( no puede contribuir a que se cumpla).

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 .

Propagación y resolución de unidades

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:

  1. la resolución es un procedimiento de refutación completo mientras que la propagación de unidades no lo es; en otras palabras, incluso si un conjunto de cláusulas es contradictorio, la propagación de unidades puede no generar una inconsistencia;
  2. las dos cláusulas que se resuelven no pueden, en general, eliminarse después de que la cláusula generada se agrega al conjunto; por el contrario, la cláusula no unitaria involucrada en una propagación unitaria puede eliminarse cuando su simplificación se agrega al conjunto;
  3. La resolución en general no incluye la primera regla utilizada en la propagación de unidades.

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 .

Utilizando un modelo parcial

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.

Complejidad

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.

Véase también

Referencias