 |
darkshadow |
Are You From The Past?
Registered: Jul 2007
Posts: 485 (0.07 al dì)
Location: Milano
Corso: Informatica Magistrale
Anno: 1
Time Online: 13 Days, 13:38:56 [...]
Status: Offline
Edit | Report | IP: Logged |
Esercizi di Preparazione per il 1° compito del 30/03/09
Ciao,
in vista del compito di logica del 30 che ne dite se mettiamo le soluzioni degli esercizi dei vecchi temi d'esame/compitini? Parlo della pate che riguarda l'algoritmo DPLL. Magari controllando anche che questi siano efettivamente giusti.
Ecco quelle che ho fatto io:
1) studiare mediante la procedura DPLL la soddisfacibilità del seguente insieme di clausole:
code:
C = {p V q, ¬q, r V ¬p, ¬r V s, ¬p V ¬s}
Ø ├ C
Spezzamento su p
Ramo p = 1 ├ C
p = 1 ├ {¬q, r, ¬r V s, ¬s}
p = 1, q = 0 ├ {r, ¬r V s, ¬s}
p = 1, q = 0, r = 1 ├ {s, ¬s}
p = 1, q = 0, r = 1, s = 1 ├ {□}
UNSAT
Ramo p = 0 ├ C
p = 0 ├ {q, ¬q,¬r V s}
p = 0, q = 1 ├ {¬r V s}
p = 0, q = 1, r = 0 ├ {□}
UNSAT
2) studiare mediante la procedura DPLL la soddisfacibilità del seguente insieme di clausole:
code:
C = {¬p V q, ¬s V ¬t, ¬q, p V ¬r, r V s}
Ø ├ C
q = 0 ├ {¬p, ¬s V ¬t,p V ¬r, r V s}
q = 0, p = 0 ├ {¬s V ¬t,¬r, r V s}
q = 0, p = 0, r = 0 ├ {¬s V ¬t, s}
q = 0, p = 0, r = 0, s = 1 ├ {¬t}
q = 0, p = 0, r = 0, s = 1, t = 0 ├ Ø
SAT
3) Applicando l'algoritmo DPLL, determinare se il seguente insieme di clausole è o meno soddisfacibile:
code:
C = {¬p1 V ¬p2, p2 V p3, ¬p1 V ¬p3 V p4, p2 V ¬p3 V ¬p4, p1 V p4}
Ø ├ C
Spezzamento su p1
Ramo p1 = 1 ├ C
p1 = 1 ├ {¬p2, p2 V p3, ¬p3 V p4, p2 V ¬p3 V ¬p4}
p1 = 1, p2 = 0 ├ {p3, ¬p3 V p4, ¬p3 V ¬p4}
p1 = 1, p2 = 0, p3 = 1 ├ {p4, ¬p4}
p1 = 1, p2 = 0, p3 = 1, p4 = 1 ├ {□}
UNSAT
Ramo p1 = 0 ├ C
p1 = 0 ├ {p2 V p3, p2 V ¬p3 V ¬p4, p4}
p1 = 0, p4 = 1 ├ {p2 V p3,p2 V ¬p3}
p1 = 0, p4 = 1, p2 = 1 ├ {□}
UNSAT
4) dimostrare che la seguente formula è una tautologia negandola, trasformandola in FNC e applicando l'algoritmo DPLL
(((p → q) → q) Λ ¬q) → ((r → ¬p) → ¬r)
code:
¬((((p → q) → q) Λ ¬q) → ((r → ¬p) → ¬r))
(((p → q) → q) Λ ¬q) Λ ¬(((r → ¬p) → ¬r))
((¬(p → q) V q) Λ ¬q) Λ ¬((¬(r → ¬p) V ¬r))
(((p Λ ¬q) V q) Λ ¬q) Λ ¬((r Λ p) V ¬r)
(p V q) Λ (¬q V q) Λ ¬q Λ ¬(r Λ p) Λ r
(¬q V q) = 1, si semplifica.
(p V q) Λ ¬q Λ (¬r V ¬p) Λ r
C = {p V q, ¬q, ¬r V ¬p, r}
Ø ├ C
q = 0 ├ {p, ¬r V ¬p, r}
q = 0, p = 1 ├ {¬r, r}
q = 0, p = 1, r = 1 ├ {□}
UNSAT -----> allora è una TAUTOLOGIA
5) Dimostrare che l'insieme formato dalle seguenti 5 clausole è insoddisfacibile applicando l'algoritmo DPLL
code:
C = {p V q V r, p V ¬q, q V ¬r, r V ¬p, ¬p V ¬q V ¬r}
Ø ├ C
Spezzamento su p
Ramo p = 1 ├ C
p = 1 ├ {q V ¬r, r, ¬q V ¬r}
p = 1, r = 1 ├ {q, ¬q}
p = 1, r = 1, q = 1 ├ {□}
UNSAT
Ramo p = 0 ├ C
p = 0 ├ {q V r, ¬q, q V ¬r}
p = 0, q = 0 ├ {r, ¬r}
p = 0, q = 0, r = 1 ├ {□}
UNSAT
6) Dimostrare che l'insieme formato dalle seguenti 5 clausole è insoddisfacibile applicando l'algoritmo DPLL
code:
C = {p V ¬r, r V ¬q, q V p V r, q V ¬p, ¬p V ¬q V ¬r}
Ø ├ C
Spezzamento su p
Ramo p = 1 ├ C
p = 1 ├ {r V ¬q, q, ¬q V ¬r}
p = 1, q = 1 ├ {r,¬r}
p = 1, q = 1, r = 1 ├ {□}
UNSAT
Ramo p = 0 ├ C
p = 0 ├ {¬r, r V ¬q, q V r}
p = 0, r = 0 ├ {¬q, q}
p = 0, r = 0, q = 0 ├ {□}
UNSAT
7) Applicando l'algoritmo DPLL, determinare se il seguente insieme di clausole è o meno soddisfacibile:
code:
C = {p1 V ¬p4, ¬p1 V ¬p2, p2 V p3, ¬p1 V ¬p3 V p4, p2 V ¬p3 V ¬p4, p1 V p4}
Ø ├ C
Spezzamento su p1
Ramo p1 = 1 ├ C
p1 = 1 ├ {¬p2, p2 V p3, ¬p3 V p4, p2 V ¬p3 V ¬p4}
p1 = 1, p2 = 0 ├ {p3, ¬p3 V p4, ¬p3 V ¬p4}
p1 = 1, p2 = 0, p3 = 1 ├ {p4, ¬p4}
p1 = 1, p2 = 0, p3 = 1, p4 = 1 ├ {□}
UNSAT
Ramo p1 = 0 ├ C
p1 = 0 ├ {¬p4, p2 V p3, p2 V ¬p3 V ¬p4, p4}
p1 = 0, p4 = 0 ├ {p2 V p3}
QUI COSA DEVO APPLICARE???
Questi sono quelli che ho fatto per ora. Se qualcuno vuole controllare che siano giusti e se ci sono errori posti la soluzione giusta. Inoltre mi sapete dire cosa devo fare nella 7) che a un certo punto non so cosa applicare.
Ciao e grazie a chi vorrà partecipare!
Ds.
__________________
by Ð@rk§h@ÐØw
|
darkshadow
Attachment: 
