 |
Are You From The Past?
Registered: Jul 2007
Posts: 485 (0.08 al dì)
Location: Milano
Corso: Informatica Magistrale
Anno: 1
Time Online: 13 Days, 13:38:56 [...]
Status: Offline
Edit | Report | IP: Logged |
Aiuto DPLL
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.
__________________
by Ð@rk§h@ÐØw
|
|
28-03-2008 15:34 |
|
|
| |
|
.grande:maestro.
Registered: Nov 2003
Posts: 1644 (0.22 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline
Edit | Report | IP: Logged |
Devo vedere se trovo quello che avevo studiato e a metterlo in qualche forma utilizzabile.
Di preciso che dubbi hai?
__________________
?
|
|
28-03-2008 16:04 |
|
|
| |
|
Are You From The Past?
Registered: Jul 2007
Posts: 485 (0.08 al dì)
Location: Milano
Corso: Informatica Magistrale
Anno: 1
Time Online: 13 Days, 13:38:56 [...]
Status: Offline
Edit | Report | IP: Logged |
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.
__________________
by Ð@rk§h@ÐØw
|
|
28-03-2008 16:41 |
|
|
| |
|
:D
Registered: Aug 2004
Posts: 984 (0.14 al dì)
Location: Milano
Corso: Informatica
Anno: IT IS OVER!
Time Online: 14 Days, 19:29:42 [...]
Status: Offline
Edit | Report | IP: Logged |
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.
|
|
28-03-2008 19:03 |
|
|
| |
|
.grande:maestro.
Registered: Nov 2003
Posts: 1644 (0.22 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline
Edit | Report | IP: Logged |
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.
__________________
?
Last edited by yeah on 28-03-2008 at 21:02
|
|
28-03-2008 20:20 |
|
|
| |
|
:D
Registered: Aug 2004
Posts: 984 (0.14 al dì)
Location: Milano
Corso: Informatica
Anno: IT IS OVER!
Time Online: 14 Days, 19:29:42 [...]
Status: Offline
Edit | Report | IP: Logged |
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 
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
|
|
28-03-2008 20:48 |
|
|
| |
|
.grande:maestro.
Registered: Nov 2003
Posts: 1644 (0.22 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline
Edit | Report | IP: Logged |
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
__________________
?
|
|
28-03-2008 21:04 |
|
|
| |
|
:D
Registered: Aug 2004
Posts: 984 (0.14 al dì)
Location: Milano
Corso: Informatica
Anno: IT IS OVER!
Time Online: 14 Days, 19:29:42 [...]
Status: Offline
Edit | Report | IP: Logged |
Originally posted by yeah
Ammazza quanti sono o_O
Provate a farli che li controllo
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).
|
|
28-03-2008 21:07 |
|
|
| |
|
.grande:maestro.
Registered: Nov 2003
Posts: 1644 (0.22 al dì)
Location: Cologno Monzese
Corso: Informatica Magistrale
Anno: II
Time Online: 12 Days, 21:36:41 [...]
Status: Offline
Edit | Report | IP: Logged |
Posta il procedimento che lo guardo 
__________________
?
|
|
28-03-2008 21:20 |
|
|
| |
|
:D
Registered: Aug 2004
Posts: 984 (0.14 al dì)
Location: Milano
Corso: Informatica
Anno: IT IS OVER!
Time Online: 14 Days, 19:29:42 [...]
Status: Offline
Edit | Report | IP: Logged |
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
Last edited by Simeon on 30-03-2008 at 15:26
|
|
28-03-2008 22:18 |
|
|
| |
|
Are You From The Past?
Registered: Jul 2007
Posts: 485 (0.08 al dì)
Location: Milano
Corso: Informatica Magistrale
Anno: 1
Time Online: 13 Days, 13:38:56 [...]
Status: Offline
Edit | Report | IP: Logged |
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.
__________________
by Ð@rk§h@ÐØw
|
|
29-03-2008 08:13 |
|
|
| |
|
.consigliere.
Registered: Oct 2007
Posts: 114 (0.02 al dì)
Location:
Corso:
Anno:
Time Online: 20:21:35 [...]
Status: Offline
Edit | Report | IP: Logged |
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.
Last edited by Larios on 29-03-2008 at 14:07
|
|
29-03-2008 14:03 |
|
|
| |
|
.consigliere.
Registered: Oct 2007
Posts: 114 (0.02 al dì)
Location:
Corso:
Anno:
Time Online: 20:21:35 [...]
Status: Offline
Edit | Report | IP: Logged |
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? 
|
|
29-03-2008 14:22 |
|
|
| |
|
:D
Registered: Aug 2004
Posts: 984 (0.14 al dì)
Location: Milano
Corso: Informatica
Anno: IT IS OVER!
Time Online: 14 Days, 19:29:42 [...]
Status: Offline
Edit | Report | IP: Logged |
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
Se il procedimento e' giusto penso vada bene uguale.
|
|
29-03-2008 14:55 |
|
|
| |
|
.consigliere.
Registered: Oct 2007
Posts: 114 (0.02 al dì)
Location:
Corso:
Anno:
Time Online: 20:21:35 [...]
Status: Offline
Edit | Report | IP: Logged |
ok
per quel che riguarda l'esercizio svolto di yeah è giusto?
|
|
29-03-2008 15:05 |
|
|
| |
|
| All times are GMT. The time now is 05:50. |
|
|
 |
|
 |
|
|
| |
Forum Rules:
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts
|
HTML code is OFF
vB code is ON
Smilies are ON
[IMG] code is ON
|
|
|
|
|
|
