Resolution (Logic)

logic

Definition

Resolution (Logic)

Resolution is an inference rule and proof method used to determine if a set of logical formula is unsatisfiable. It is a sound and complete proof method, meaning it makes correct inferences and can derive any entailed sentence, especially for propositional logic.

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