3
$\begingroup$

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

enter image description here

$\endgroup$
2
$\begingroup$

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

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

  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.

$\endgroup$
  • $\begingroup$ 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 .. $\endgroup$ – displayname Nov 14 '13 at 20:22
  • $\begingroup$ As I wrote, this must be given. It cannot be derived.\ $\endgroup$ – Johannes Kloos Nov 15 '13 at 7:42
  • $\begingroup$ You are right! Now I got it .. I really was wondering how this works but you got confirmed by my professor! $\endgroup$ – displayname Nov 15 '13 at 10:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.