Regla de resolución

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{p,q,\neg r\}\qquad \{r, s, \neg t\}}{\{p,q, s, \neg t\}}$$

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{\neg p,q\}\qquad \{\neg q\}}{\{\neg p\}}$$

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{p,q,\neg r\}\qquad \{\neg p, r, s\}}{\{p,q, \neg p, s\}}$$

El resolvente es la cláusula trivial

Algunos ejemplos

$$\dfrac{C_1\qquad C_2}{(C_1-\{\ell\}) \cup (C_2-\{\ell^c\})}$$

$$\dfrac{\{s\}\qquad \{\neg s\}}{\square}$$

Algunos ejemplos

$$\dfrac{\{s\}\qquad \{\neg s\}}{\square}$$

• La cláusula vacía es una disyunción entre elementos nulos, ¡uno de ellos debe satisfacerse para que $\square$ también se satisfaga!
• La cláusula vacía se satisface siempre que $s$ y $\neg s$ se satisfagan.
• La cláusula vacía es insatisfasible.

El resolvente $C$ es satisfacible syss las cláusulas padre $C_1$ y $C_2$ son ambas satisfacibles.

• $\boxed{\rightarrow}$ Sea $I$ una interpretación que satisface a $C$, $I(\ell^{\diamond})=1$ para al menos alguna literal $\ell^{\diamond}\in C$.
• Si $\ell^{\diamond}\in C_1$, $I(C_1)=1$.
• Como $\ell\not\in C$ ni $\ell^c\not\in C$, $I$ no está definida en $\ell$ o $\ell^c$. Extendemos $I$ a $I'$ definiendo $I'(\ell^c)=1$. Puesto que $\ell^c\in C_2$, tenemos $I'(C_2)=1$; además $I'(C_1)=I(C_1)=1$.
• Por lo tanto, $I'$ es un modelo para $C_1$ y $C_2$. Análogamente cuando $\ell^{\diamond}\in C_2$.

El resolvente $C$ es satisfacible syss las cláusulas padre $C_1$ y $C_2$ son ambas satisfacibles.

• $\boxed{\leftarrow}$ Sean $C_1$ y $C_2$ satisfacibles por la interpretación $I$.
• Como $\ell$ y $\ell^c$ son complementarias, se tiene que $I(\ell)=1$, o bien, $I(\ell^c)=1$.
• Supongamos que $I(\ell)=1$, entonces $I(\ell^c)=0$ y $C_2$, la cláusula que contiene a $\ell^c$, se satisface porque hay otra literal $\ell'\in C_2$ ($\ell'\neq \ell^c$) tal que $I(\ell')=1$.
• Por construcción de la regla de resolución, $\ell'\in C$, de modo que $I$ también es un modelo de $C$. Análogamente cuando $I(\ell^c)=1$.

Algoritmo (resolución binaria)

Input: Un conjunto de cláusulas $S$.
Output: $S$ es satisfacible o insatisfacible.

Definimos $S_0=S$.

Repetir los siguientes pasos para obtener $S_{i+1}$ a partir de $S_i$:

• Escoja cláusulas de colisión $\{C_1, C_2\}\subseteq S_i$ que no se hayan escogido anteriormente.

Algoritmo (resolución binaria. Continuación.)

• Encuentre $C=\mathsf{Res}(C_1, C_2)$ de acuerdo a la regla de resolución.
• Si $C$ no es una cláusula trivial, $S_{i+1}=S_i\cup\{C\}$; de otro modo, $S_{i+1}=S_i$.

Hasta que $C=\square$, en cuyo caso $S$ es insatisfacible; o hasta que la regla de resolución se haya aplicado a todos los pares de cláusulas de colisión, lo que indica que $S$ es satisfacible.

Proposición

Si un conjunto de cláusulas $S=\{\varphi_1,\varphi_2,\ldots,\varphi_n\}$ ($n\geq 0)$ es satisfacible, entonces cualquier conjunto $S_i$ ($i\geq 0$), generado por el algoritmo de resolución binaria, es satisfacible.