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.