Resolution Inference Rule (Propositional Resolution)

propositional-logic

Definition

Resolution Inference Rule (Propositional Resolution)

$${\frac{C\vee p\neg p\vee D}{C\vee D}}_{(\text{resolution})}$$

where $C\vee D$ is called the the resolvent and $p$ is called resolved atom.

Examples

Example

Given a Boolean function in CNF:

$$\begin{array}{r}f(x,y,z)=\underset{=C_1}{\underbrace{(\neg x\vee \neg y\vee \neg z)}}\wedge \underset{=C_2}{\underbrace{(\neg x\vee y\vee \neg z)}}\wedge \underset{=C_3}{\underbrace{(\neg x\vee y\vee z)}}\wedge \\ \underset{=C_4}{\underbrace{(\neg x\vee \neg y\vee z)}}\wedge \underset{=C_5}{\underbrace{(x\vee \neg y\vee \neg z)}}\wedge \underset{=C_6}{\underbrace{(x\vee y\vee \neg z)}}\wedge \underset{=C_7}{\underbrace{z}}\end{array}$$

The unit clause is $C_7=z$. Find all clauses that contain $\neg z$, the complement of $C_7$:

1. $C_1=\neg x\vee \neg y\vee \neg z$, then the resolvent is $C_8=\neg x\vee \neg y$
2. $C_2=\neg x\vee y\vee \neg z$, then the resolvent is $C_9=\neg x\vee y$
3. $C_5=x\vee \neg y\vee \neg z$, then the resolvent is $C_{10}=x\vee \neg y$
4. $C_6=x\vee y\vee \neg z$, then the resolvent is $C_{11}=x\vee y$

From there, we continue:

1. $C_8=\neg x\vee \neg y$ and $C_9=\neg x\vee y$, then the resolvent is $C_{12}=\neg x$
2. $C_{10}=x\vee \neg y$ and $C_{11}=x\vee y$, then the resolvent is $C_{13}=x$

The resolvent of $C=12$ and $C=13$ is an empty clause. If an empty clause is found, then the Boolean function is unsatisfiable:

$$\cancel{\models }f(x,y,z)$$

Example

$$\neg p\vee q,p\vee r,\neg q\vee s⊢r\vee s$$

Example

$$\cancel{⊢}p\vee \neg p$$