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


I'm not quite certain what your actual question is, but:


*

*The lower part of the page you scanned shows a resolution proof. I haven't checked every step, but at least the lower part looks correct.

*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.
