 | |
Il progetto dsy.it è l'unofficial support site dei corsi di laurea del Dipartimento di Scienze dell'Informazione e del Dipartimento di Informatica e Comunicazione della Statale di Milano. E' un servizio degli studenti per gli studenti, curato in modo no-profit da un gruppo di essi. I nostri servizi comprendono aree di discussione per ogni Corso di Laurea, un'area download per lo scambio file, una raccolta di link e un motore di ricerca, il supporto agli studenti lavoratori, il forum hosting per Professori e studenti, i blog, e molto altro...
In questa sezione è indicizzato in textonly il contenuto del nostro forum |
Aiuto DPLL
Clicca QUI per vedere il messaggio nel forum |
| darkshadow |
Ciao ragazzi.
Ho saltato le ultime lezioni di logica in cui ha spiegato le DPLL.
Qualcuno puo' gentilmente fare qualche esempio di come funziona??
magari commentando l'esercizio in modo tale da capire come si fanno.
Ho dato uno sguardo sulle dispense ma ci sono solo delle formule e gli esercizi non vengono commentati quindi è difficile capire come funziona.
Grazie in anticipo. |
| yeah |
Devo vedere se trovo quello che avevo studiato e a metterlo in qualche forma utilizzabile.
Di preciso che dubbi hai? |
| darkshadow |
so che bisogna prima fare la fnn poi la fnc e poi fare la dpll. Le prime due le so invece la dpll non l'ho proprio capita perchè nelle dispense fa vedere degli esempi ma non spiega i passaggi che fa.
se riesci a postare qualche esempio commentandolo mi fai un grande favore. |
| Simeon |
Dopo che hai aiutato darkshadow potresti dirmi come ti muoveresti in questa situazione, per favore?
p1=0 - {¬p4, p2 V p3, p2 V ¬p3 V ¬p4, p4}
la cosa che non mi convince e' la presenza di ¬p4 e p4. non so se posso proseguire normalmente o fermarmi dichiarando l'insoddisfacibilita' (se non ci fossero le altre clausole di mezzo farei cosi').
@darkshadow : non so se ti possa essere d'aiuto, ma ai tempi io usai
http://homes.dsi.unimi.it/~zucchell.../SlidesDPLL.pdf per capire la DPLL. Sono gli stessi lucidi che si trovano sul sito, ma lo svolgimento della DPLL e' commentato e piu' chiaro. |
| yeah |
la cosa che non mi convince e' la presenza di ¬p4 e p4. non so se posso proseguire normalmente o fermarmi dichiarando l'insoddisfacibilità (se non ci fossero le altre clausole di mezzo farei cosi').
Sì, alla fine dovresti ottenere la clausola vuota, soltanto che devi continuare ad applicare le regole fino in fondo. Prosegui applicando l'asserzione e poi la risoluzione unitaria :)
Ricorda che è un algoritmo, quindi anche se ad intuito si capisce che non è soddisfacibile, devi comunque proseguire finché ottieni la clausola vuota da tutti i rami della procedura.
Le prime due le so invece la dpll non l'ho proprio capita perchè nelle dispense fa vedere degli esempi ma non spiega i passaggi che fa.
Ok, dalla FNC ottieni qualcosa come: C1 ^ C2 ^ C3, queste le traduci nell'insieme di clausole C={C1, C2, C3}.
La DPLL mira a trovare un assegnamento (anche parziale) che soddisfi l'insieme di clausole, cioè le tue Ci saranno scritte impiegando diverse lettere proposizionali (p, q, r, ...) e con la DPLL arrivi ad ottenere qualcosa come {p = 1, q = 1, r = 0, ...} col quale tutte le clausole dell'insieme sono soddisfatte (cioè valgono vero), oppure hai la clausola vuota e C è insoddisfacibile.
Questo e' un esercizio che avevo fatto, c'è solo una parte (infatti al primo passo ho fatto uno spezzamento di cui ho poi verificato solo una parte), dimmi come ti trovi.
In sostanza, per applicare una regola devi verificare che il tuo insieme di clausole te lo consenta, ad esempio la sussunzione:
V |- C u {p v C}
----------------------------- (col vincolo che devi avere già p=1)
V |- C
significa che passi da {p = 1} |- {p v q, r} a {p=1} |- {r}
in pratica, dato che hai già deciso per p=1, la clausola che contiene p (essendo una disgiunzione di letterali) sarà sempre soddisfatta per p=1, indipendentemente dal valore assunto dagli altri letterali. |
| Simeon |
Originally posted by yeah
Sì, alla fine dovresti ottenere la clausola vuota, soltanto che devi continuare ad applicare le regole fino in fondo. Prosegui applicando l'asserzione e poi la risoluzione unitaria :)
Hai ragione, cosi' facendo mi rimane
p1=0,p4=0 - {p2 V p3, (clausola vuota)}
e proseguendo avrei
p1=0,p4=0,p2=1,p3=1 - clausola vuota
ti ringrazio nuovamente :asd:
Se ti dovesse avanzare un attimo di tempo e voglia prima di lunedi' mi farebbe molto piacere se potessi risolvere alcuni esercizi su DPLL, potrebbe essere d'aiuto anche ad altri.
Li copio qua, poi fai come vuoi
1)
code:
¬p V s, p V q, p V r, p V ¬q V ¬t, ¬p V ¬s, ¬r V t
2)
code:
¬p v s v r, p v q, p v r, ¬q v ¬s v p, ¬p v ¬s
3)
code:
¬p V s, p V q, p V r, ¬q V ¬r V p, ¬p V ¬s
|
| yeah |
Se ti dovesse avanzare un attimo di tempo e voglia prima di lunedi' mi farebbe molto piacere se potessi risolvere alcuni esercizi su DPLL, potrebbe essere d'aiuto anche ad altri.
Ammazza quanti sono o_O
Provate a farli che li controllo :asd: |
| Simeon |
Originally posted by yeah
Ammazza quanti sono o_O
Provate a farli che li controllo :asd:
Io li ho fatti ma di quei tre in particolare mi sembra di sbagliare il procedimento, per questo sarebbe stato comodo che tu li risolvessi.
Poi oh, se non ti va non importa, ma era il procedimento che contava (almeno per me). |
| yeah |
| Posta il procedimento che lo guardo ;) |
| Simeon |
Bon, li copio dal quad ( i passaggi di sussunzione e risoluzione unitaria sono impliciti )
code:
¬p V s, p V q, p V r, p V ¬q V ¬t, ¬p V ¬s, ¬r V t
asserzioni e letterali puri non se ne possono fare, spezzo su p:
[RAMO p=1]
p=1 - {s,¬s,¬r V t}
letterale puro per r
p=1,r=0 - {s,¬s} (qui non mi convinceva la sparizione di t e l'applicazione del letterale puro)
asserzione su s e ris. unitaria su ¬s
p=1,r=0,s=1 - clausola vuota
[RAMO p=0]
p=0 - {q,r,¬q V ¬t,¬r V t}
asserzione su q
p=0, q=1 - {r,¬t,¬r V t}
asserzione su r
p=o, q=1, r=1 - {¬t,t}
asserzone su t
P=0, q=1, r=1, t=1 - clausola vuota
Insoddisfacibili entrambi i rami
code:
¬p v s v r, p v q, p v r, ¬q v ¬s v p, ¬p v ¬s
qui c'e' r e non c'e' ¬r, per cui applico il letterale puro (e' giusto?)
r=1 - {pvq,¬q V ¬s V p, ¬p V ¬s}
spezzo su p
[RAMO p=1]
r=1,p=1 - {¬s}
asserzione su ¬s
r=1,p=1,s=0 (q e' sparita, va bene l'assegnamento parziale?)
[RAMO p=0]
r=1,p=0 - {q,¬q V ¬s}
asserzione su q
r=1,p=0,q=1 - {¬s}
asserzione su ¬s
r=1,p=0,q=1,s=1
Vengono due assegnamenti, di cui uno parziale
code:
¬p V s, p V q, p V r, ¬q V ¬r V p, ¬p V ¬s
niente asserzioni o letterali puri, spezzo su p
[RAMO p=1]
p=1 - {s,¬s} (q sparisce... boh=
asserzione su s
p=1,s=1 - {¬s}
ris. unitaria su s
p=1,s=1 - clausola vuota
[RAMO p=0]
p=0 - {q,r,¬q V ¬r}
asserzione su q
p=0, q=1 - {r,¬r}
asserzione su r
p=0, q=1, r=1 - {¬r}
ris. unitaria su ¬r
p=0, q=1, r=1 - clausola vuota
insoddisfacibili entrambi i rami
EDIT: corretta lettera eser. 2 |
| darkshadow |
grazie ragazzi.
non ho ancora avuto tempo di guardare bene perchè sono un po' impegnato ma più tardi lo farò, e se avro' dei dubbi li postero'.
grazie ancora. |
| Larios |
ho provato a fare gli esercizi ma non ho capito perchè sullo spezzamento del primo esercizio una volta ottenuto:
p=1 - {s,¬s,¬r V t}
fai -> letterale puro per r
nel senso non capisco perchè prendi prima ¬r di s non mi pare ci siano precedenze di questo genere da rispettare sugli appunti, se ho capito male in caso contrario devo prendere il primo elmento che è o 1 o 0 corretto?
il secondo e terzo mi vengono anche a me cosi. |
| Larios |
Originally posted by yeah
All'inizio non si puo applicare nulla quindi applico lo spezzamento su p. Perchè sul secondo ramo non compare p=0 ma q=0.
Sicuro che è corretto? :? |
| Simeon |
Originally posted by Larios
[B]ho provato a fare gli esercizi ma non ho capito perchè sullo spezzamento del primo esercizio una volta ottenuto:
p=1 - {s,¬s,¬r V t}
fai -> letterale puro per r
nel senso non capisco perchè prendi prima ¬r di s non mi pare ci siano precedenze di questo genere da rispettare sugli appunti, se ho capito male in caso contrario devo prendere il primo elmento che è o 1 o 0 corretto?
Mah, l'ho fatto senza nessuna ragione particolare, volendo avrei potuto prendere prima s e farci l'asserzione, ma poi mi rimaneva la clausola vuota tra le palle e l'ho lasciata per ultima :asd:
Se il procedimento e' giusto penso vada bene uguale. |
| Larios |
ok :)
per quel che riguarda l'esercizio svolto di yeah è giusto? |
| yeah |
----- Primo esercizio di Simeon -----
p=1,r=0 - {s,¬s} (qui non mi convinceva la sparizione di t e l'applicazione del letterale puro)
Dal momento che avevi (not) r e r=0, ti rimaneva t per risoluzione unitaria (regola 2.3); a parte quel passaggio, il risultato è giusto per quel ramo.
E' giusto anche il secondo ramo.
----- Secondo esercizio di Simeon -----
qui c'e' r e non c'e' ¬r, per cui applico il letterale puro (e' giusto?)
Giusto, ah nel passaggio subito è comparso (not) r anziché (not) s, sicuramente un errore di battitura, lo scrivo per altri che potrebbero leggerlo :)
r=1 - {pvq,¬q V ¬s V p, ¬p V ¬s}
spezzo su p
Non è formalmente sbagliato, però lo spezzamento è meglio tenerlo come ultima spiaggia, e applicare prima tutte le altre, se si può. Dal momento che avevi (not) s e non avevi s, potevi applicare il letterale puro ottenendo:
r=1,s=0 - {pvq,¬q V ¬s V p, ¬p V ¬s}
r=1,s=0 - {pvq}
E fare lo spezzamento qui.
Dal momento che le regole possono essere applicate in modo sparso, si possono ottenere percorsi diversi, ciò che conta è il risultato finale, che deve essere uguale.
(Non ho capito se questo è un dubbio o no :)) Ottenere un assegnamento parziale è perfettamente lecito, se provi ad usarlo nell'insieme di clausole di partenza vedrai che, benché esso manchi di alcune lettere proposizionali, soddisfa comunque le clausole.
----- Terzo esercizio di Simeon -----
[RAMO p=1]
p=1 - {s,¬s} (q sparisce... boh=
q non "sparisce", ma si trova in una clausola in cui compare anche p e poiché a p hai assegnato 1, la clausola in cui compare q è soddisfatta qualsiasi sia il valore di verità che le assegneresti (dal momento che è in OR con p).
Il resto è corretto.
Mah, l'ho fatto senza nessuna ragione particolare, volendo avrei potuto prendere prima s e farci l'asserzione, ma poi mi rimaneva la clausola vuota tra le palle e l'ho lasciata per ultima :asd:
Se il procedimento e' giusto penso vada bene uguale.
E' giusto, le regole si possono applicare nell'ordine che si preferisce, infatti conviene applicarle in modo da facilitarsi i conti :)
All'inizio non si puo applicare nulla quindi applico lo spezzamento su p. Perchè sul secondo ramo non compare p=0 ma q=0.
Sicuro che è corretto?
Quello che vedi è un secondo spezzamento, su q :). Dello spezzamento iniziale ho svolto solo un ramo, con p=1. L'altro (nel rettangolo vuoto) non c'è. Ho preferito postare questo esercizio piuttosto che un altro che era lungo il doppio, perché il procedimento è sempre lo stesso, serve acquisire un po' di dimestichezza con le regole (che è meglio sappiate riscriverle senza guardare gli appunti). |
| Larios |
si poi mi sono accorto... grazie :)
solo un dubbio, ma se vedo che il primo ramo di uno spezzamento è soddisfacibile non è finito l'esercizio?
in questo caso nel 2) si puo applicare nuovamente il letterale puro e dimostare che è sodisfacibile, senza usare lo spezzamento, o sbaglio?
r=1,s=0 - {pvq}
E fare lo spezzamento qui.
|
| yeah |
solo un dubbio, ma se vedo che il primo ramo di uno spezzamento è soddisfacibile non è finito l'esercizio?
Sì, mentre se ti risulta la clausola vuota devi andare avanti finché i rami ti risultano insoddisfacibili :) |
| Simeon |
Originally posted by yeah
Dal momento che avevi (not) r e r=0, ti rimaneva t per risoluzione unitaria (regola 2.3); a parte quel passaggio, il risultato è giusto per quel ramo.
Eh no scusa, se ho r=0 su ¬r si usa la sussunzione, per cui sparisce l'intera clausola ¬r V t. O no?
Giusto, ah nel passaggio subito è comparso (not) r anziché (not) s, sicuramente un errore di battitura, lo scrivo per altri che potrebbero leggerlo :)
Si, ora l'ho corretto :)
Non è formalmente sbagliato, però lo spezzamento è meglio tenerlo come ultima spiaggia, e applicare prima tutte le altre, se si può. Dal momento che avevi (not) s e non avevi s, potevi applicare il letterale puro ottenendo:
r=1,s=0 - {pvq,¬q V ¬s V p, ¬p V ¬s}
r=1,s=0 - {pvq}
E fare lo spezzamento qui.
Vero, tnx (se ho ben capito questo e' l'unico vero errore, in quanto DOVEVO usare il letterale puro prima dello spezzamento).
Dal momento che le regole possono essere applicate in modo sparso, si possono ottenere percorsi diversi, ciò che conta è il risultato finale, che deve essere uguale.
Appunto, quindi il mio primo esercizio dovrebbe risultare corretto (e non ho capito se e' cosi' o meno)
q non "sparisce", ma si trova in una clausola in cui compare anche p e poiché a p hai assegnato 1, la clausola in cui compare q è soddisfatta qualsiasi sia il valore di verità che le assegneresti (dal momento che è in OR con p).
E quindi e' giusto ? Se poi mi scrivi "il resto e' corretto" non capisco (sti esercizi sono troppo soggetti a errori del cazzo, per questo vado in paranoia e servono conferme :asd: )
Ah giusto:
=1,s=0 - {pvq}
E fare lo spezzamento qui.
Perche' spezzamento? abbiamo p e non abbiamo ¬p, abbiamo q e non abbiamo ¬q, non si puo' semplicemente applicare il letterale puro a uno dei due? Lo spezzamento si fa quando non si puo' fare altro no?
Cioe' riassumendo, di SBAGLIATO ci dovrebbe essere solo l'esercizio 2 in quanto ho applicato lo spezzamento quando si poteva fare il letterale puro (anche se poi il risultato veniva giusto uguale). |
| darkshadow |
una cosa sul es. 2 dopo aver arrivato a:
r = 1, s = 0 - {p V q} applico il letterale puro su p ed ottengo:
r = 1, s = 0, p = 1 che la rende soddisfacibile.
ma q?? il suo vale è indifferente??
stessa cosa avviene se invece di p prendo q. |
| Bisciu |
se ti rimane p V q assegni a p il valore 1. per il letterale puro a questo punto riscrivi p V q e il passaggio successivo cancelli l'intera clausola perchè se hai p V q e p è vera allora di conseguenza lo è anche q.
detto in termini logici.
r = 1, s = 0 - {p V q} applico il letterale puro su p ed ottengo:
r = 1, s = 0, p = 1 - {p v q} applico quindi una sussunzione ed ho:
r = 1, s = 0, p = 1 - zero quindi sat
ciao |
| darkshadow |
per quanto riguarda la teoria?? c'e' nel compito??
per esempio in un compito c'e' questo esercizio:
Sia A V B una contraddizione e sia r una lettera proposizionale. Allora
1) il sequente A ----> r è dimostrabile
2) il sequente r ----> A è dimostrabile
3) il sequente r ----> A V B è dimostrabile
come si fa?? |
| Simeon |
Originally posted by darkshadow
per quanto riguarda la teoria?? c'e' nel compito??
per esempio in un compito c'e' questo esercizio:
Sia A V B una contraddizione e sia r una lettera proposizionale. Allora
1) il sequente A ----> r è dimostrabile
2) il sequente r ----> A è dimostrabile
3) il sequente r ----> A V B è dimostrabile
come si fa??
Dimostrabile ? Cos'e' quella roba ? :o
Magari hai guardato a compiti PARECCHIO vecchi. |
| darkshadow |
Originally posted by Simeon
Dimostrabile ? Cos'e' quella roba ? :o
Magari hai guardato a compiti PARECCHIO vecchi.
No. è il tema d'esame di giugno 2006. |
| yeah |
Eh no scusa, se ho r=0 su ¬r si usa la sussunzione, per cui sparisce l'intera clausola ¬r V t. O no?
Ops! Hai ragione tu, svista terribile da parte mia.
E quindi e' giusto ? Se poi mi scrivi "il resto e' corretto" non capisco
Sì, sì, è giusto :)
Perche' spezzamento? abbiamo p e non abbiamo ¬p, abbiamo q e non abbiamo ¬q, non si puo' semplicemente applicare il letterale puro a uno dei due? Lo spezzamento si fa quando non si puo' fare altro no?
Oh cavolo... promemoria: mai correggere tre esercizi di fila! Altra svista mia :-/
ma q?? il suo vale è indifferente??
Sì, ottieni in questo modo un assegnamento parziale, che comunque ti soddisfa l'insieme di clausole. |
| Simeon |
Originally posted by darkshadow
No. è il tema d'esame di giugno 2006.
Niente ho dato un occhio, e' roba del calcolo dei sequenti che non ci sara' domani.
Grazie yeah per l'aiuto :) |
| yeah |
Di nulla.
Auguri per l'esame :) |
| Snakethesniper |
Salve a tutti, avrei bisogno di una mano sempre riguardo DPLL. Quello che non riesco a comprendere è quali regole utilizzare, questo perchè non riesco a "tradurre" la notazione. Per esempio nella sussunzione, nel caso di I(p)=1 si ha:
I |- C U (p V C)
____________
I |- C
dove C rappresenta l'insieme delle clausole C.
Quello che non capisco è cosa intende per (pVC), come riconosco in un insieme di clausole se mi trovo in questa situazione?
Grazie |
| michele.c |
| p V altra roba: se p è vero, nell'or il risultato finale è in ogni caso vero, e puoi cancellare tutta la clausola. |
| Snakethesniper |
Originally posted by michele.c
p V altra roba: se p è vero, nell'or il risultato finale è in ogni caso vero, e puoi cancellare tutta la clausola.
mmm capito, ma allora perchè usare "C" quando mi viene detto a più riprese che con "C" si intendono le clausole?
Poi in un esempio arriva ad avere:
P1=1 P2=2 |- {notP2} e usa la risoluzione unitaria. Perchè? Non dovrebbe usare l'asserzione che dice I |- C U {notP} ?
E altra cosa, quel {pVC} intende che è una disgiunzione tra un letterale e un "qualcosa" C? O che può esserci un letterale p e un "qualcosa" C? |
| michele.c |
Clausola = disgiunzione di letterali. É giusto p V C, pensa a C come ad una clausola astratta dove ci sono altri letterali in disgiunzione.
L'esempio non l'ho capito, comunque a volte usando diverse regole si può arrivare allo stesso risultato, non ti puntare su di esso: punta piuttosto sul capire l'applicazione delle regole.
{pVC}: disgiunzione tra un letterale e un "qualcosa" C, dove però appunto C potrebbe essere la clausola vuota (nel senso che alla fine hai solo il letterale p) |
|
|
|
|
