.dsy:it. - Esercizi di Preparazione per il 1° compito del 30/03/09

.dsy:it.
//www.dsy.it

Esercizi di Preparazione per il 1° compito del 30/03/09

Posted by darkshadow on 22-03-2009 20:19

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.