# DPLL Algorithm $\rightarrow$ Resolution proof $\rightarrow$ Craig Interpolation

I really need help here for an exam that I got tomorrow ..

Let's say I got a bunch of constraints:

$c1 = { \lnot a \lor \lnot b } \\ c2 = { a \lor c } \\ c3 = { b \lor \lnot c } \\ c4 = { \lnot b \lor d } \\ c5 = { \lnot c \lor \lnot d } \\ c6 = { c \lor e } \\ c7 = { c \lor \lnot e } \\$

As I perform the DPPL-Algorithm on these constrains the result is, that these constraints are unsatisfiable. However, I have to show a resolution proof.

Just for convenience you can take a look at this proof (see picture below).

The thing that's left to do is to compute the Craig-Interpolation - which is not really that hard - but I don't know how to define the quantities $\varphi_1$ and $\varphi_2$.

For this example I know that

$\varphi_1 = \{ c_1, c_2, c_3, c_5 \}$ and $\varphi_2 = \{ c_4, c_6, c_7 \}$

But I don't know how I can come up with that. Can anybody help me here?

PS: Feel free to add some keywords to this question. The keywords "McMillan-Interpolation", "DPLL-Algorithm", etc. do not exist yet ..

EDIT: There is a little error in my notes: The arrows that point from DPLL to those graphs $\rightarrow$ the $\lnot a$ is $a$ and the other respectively not $a$ but $\lnot a$.

2. About choosing the variable sets in Craig interpolation: It is not possible to come up with these sets out of thin air - they must be given. The reason for this is that the Craig Interpolation Theorem is stated like this: Let $\varphi_1$ and $\varphi_2$ be formulas such that $\varphi_1 \land \varphi_2$ is unsatisfiable. Then there is a formula $\varphi_i$ such that $\varphi_1 \models \varphi_i$ and $\varphi_i \land \varphi_2$ is unsatisfiable. If you don't know the formulas $\varphi_1$ and $\varphi_2$, the theorem cannot be applied.
• Hi Johannes! Well, the forumla $\varphi = c_1 \land c_2 \land \dots \land c_7$. That's all that is given. I have the solution of the craig interpolation and there it says that (using your notation) $\varphi_1 = \{ c_1, c_2, c_3, c_5 \}$ and $\varphi_2 = \{ c_4, c_6, c_7 \}$. The thing is, that I don't know how exactly those constraints were assigned .. – displayname Nov 14 '13 at 20:22