# Solutions for exams

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Solutions for exams
Can we expect the missing solutions for some exams to be published before our exam?
Espacially the proofs are a little frustrating, because there are already not to many tasks avaible to practice…
Solutions missing:
WS1617 3.3
WS1617 retake 4.1 & 4.3
WS1718 5.2
WS19/20 4

2 Likes

Realistically, that’s going to be difficult.

I’ll have a look by Friday but am not promising.

Here is what i have. No warranty! Feel free to correct WS1617 3.3
V = {vi | i ∈ {1, …, 50}}
∀v∈V: D = Dv = {1, …, 50}
∀ui,uj∈V: C_ui,uj = C_uj,ui = {(di, dj) ∈ D x D | di = dj} for: di ≠ dj ∧ |i-j| ≠ |di-dj|

WS1617 retake 4.1
1 (A∧B∧C)⇒(A ⇒ B∧C)^F
2 (A∧B∧C)^T
3 (A⇒B∧C)^F
4 A^T
5 B^T
6 C^T
7 A^T
8 B∧C^F
9 B^F | C^F
10 ⊥ | ⊥

WS1617 retake 4.3 (looks terrible)
1 (X∧Y)∨(X∧¬Y)⇒Xf
2 (X∧Y)∨(X∧¬Y)t ; Xf
3 (X∧Y)t ∨(X∧¬Y)t ; Xf
4 Xt∨(X∧¬Y)t ; Yt∨(X∧¬Y)t ; Xf
5 Xt∨Xt ; Xt∨¬Yt ; Yt∨Xt ; Yt∨¬Yt ; Xf
6 Xt ; Xt∨Yt ; Yt∨Xt ; Yt∨Yf ; Xf
clauses: {Xt} {Xt, Yf} {Yt, Xt} {Yt, Yf} {Xf}
{Xt} + {Xf} → {}

WS17/18 5.2 (looks even more terrible)
1 ∃X((∃Y¬P(Y, f(b))) ∨ ¬(P(b, f(X)) ⇒ ¬P(g(a), f(X)))^F
2 ((∃Y¬P(Y, f(b))) ∨ ¬(P(b, f(V)) ⇒ ¬P(g(a), f(V)))^F
3 (∃Y¬P(Y, f(b))^F
4 ¬(P(b, f(V)) ⇒ ¬P(g(a), f(V)))^F
5 P(b, f(V)) ⇒ ¬P(g(a), f(V))^T
6 ¬P(W, f(b))^F
7 P(W, f(b))^T
8 P(b, f(V))^F | ¬P(g(a), f(V)))^T
9 ⊥:[b/W],[b/V] | P(g(a), f(V)))^F
10 | (not closable!)

WS19/20 4

1. q2={1}, q3={2, 4}, q4={1,2,4}
2. A variable u is arc-consistent relative to another variable v if either there are no constraints between u and v or ∀d ∈ Du there is at least one d’ ∈ Dv
such that (d, d’) ∈ C.

AfterQ2→Q1: q2={1}, q3={1, 2, 3, 4}, q4={1, 2, 3, 4}
AfterQ3→Q1: q2={1}, q3={2, 4}, q4={1, 2, 3, 4}
AfterQ2→Q3: q2={1}, q3={2, 4}, q4={1, 2, 3, 4}
AfterQ3→Q2: q2={1}, q3={4}, q4={1, 2, 3, 4}
4. When the whole constraint network is arc-consistent

1 Like

Thank you very much Bsanchez for your solutions! I got the same results as you except for in WS 17/18 5.2.
The Tableaux should be closable, you could apply the ∃^F (3-6) again in the right branch and get yourself a ¬P(Z,f(b))^F for example ( I marked my changes red):

7 P(W, f(b))^T
8 P(b, f(V))^F | ¬P(g(a), f(b)))^T
9 ⊥:[b/W],[b/V] | P(g(a), f(b)))^F
10 | ¬ P(Z, f(b)) ^F (from line 3)
11 | P(Z, f(b)) ^T
12 | ⊥:[g(a)/ Z]

It is explained in this video nugget: https://www.fau.tv/clip/id/26912

Hello matze123, no problem i hoped actually that someone would correct me on this problem. So thank you too! I mixed up the multiplicity characteristics with existsT and existsF. Your correction looks good to me.

EDIT:
maybe line 10 should be turned in P(Z, f(b))^T first, but that’s just a small thing …

Its always best to debate about solutions, that’s what’s really missing in the whole online semester… You’re right about the last step, I corrected it.

2 Likes

WS19/20 4

1. … shouldn’t Q4={2,4}, since Q2 is already assigned by 1?

nevermind! the only assignment happening (in terms of forward checking) is Q1 ← 3 (I guess)

correct, that’s why arc-consistency subsumes forward checking