Posterior: Resolución lineal Arriba: Procedimientos de demostración automática Anterior: Representación matricial

Algoritmo de Davis y Putnam

Dada $\phi = \bigwedge_i \bigvee_j \ell_{ij}$, sea $M_{\phi} = \left(\ell_{ij} \right)_{ij}$ la matriz de literales. $\ell$ aparece como LITERAL AISLADA si hay una cláusula que consiste sólo de $\ell$, es decir, si hay un renglón de $M_{\phi}$ que consta tan solo de $\ell$. $\ell$ aparece como LITERAL PURA si, habiendo aparecido ella en $M_{\phi}$, no aparece $\neg \ell$.

Procedimiento 4.8 (Algoritmo Davis-Putnam)  


Entrada:

Salida:




Algoritmo:

1. Literales aisladas contradictorias: Si para una misma literal $\ell$, tanto $\ell$ como $\neg \ell$ aparecen como literales aisladas, $\phi$ es una contradicción.
2. Literales aisladas: Si $\ell$ aparece aislada pero $\neg \ell$ no, hagamos
   $$\begin{eqnarray*} M_{\ell}^+ &=& \{\mbox{\rm cl\'ausulas en }M\mbox{\rm con }\e... ...cl\'ausulas en }M\mbox{\rm sin } \ell\mbox{\rm ni }\neg \ell\}. \end{eqnarray*}$$
   
   
   
   
   
   Sea $N_{\ell}^+$ el conjunto consistente de $M_{\ell}^0$ junto con el conjunto de cláusulas que se obtiene de $M_{\ell}^+$ suprimiendo toda aparición de $\ell$. Similarmente, sea $N_{\ell}^-$ el conjunto consistente de $M_{\ell}^0$ junto con el conjunto de cláusulas que se obtiene de $M_{\ell}^-$ suprimiendo toda aparición de $\neg \ell$. Entonces $M_{\ell}$ es contradicción si y sólo si $N_{\ell}$ es contradicción.
3. Literales puras: Si $\ell$ es una literal que aparece pura entonces $\phi$ es contradicción si y sólo si $N_{\ell}^-$ es contradicción, donde $N_{\ell}^-$ está definida como en la regla anterior.
4. Bifurcación: Para una literal cualquiera $\ell$, tendremos que $\phi$ es contradicción si y sólo si ambos conjuntos de clásulas $N_{\ell}^+$ y $N_{\ell}^-$ son contradicciones.

Posterior: Resolución lineal Arriba: Procedimientos de demostración automática Anterior: Representación matricial