Domande sul Modulo Tre

• Aggiungete le vostre domande in fondo alla pagina

---

solver_analyze

La funzione dovrebbe conoscere il letterale estratto dalla Pcoda per poter comporre la learnt clause, ma questo non gli e' stato passato come parametro, e dalla Pcoda ormai e' gia' stato estratto.

Come dobbiamo fare?

-- FrancescoBrandozzi - 31 May 2008

---

RISULTATI SECONDO MODULO

All'inidirizzo:

http://www.dsi.uniroma1.it/~parisi/handouts/risultati2.html

sono disponibili i risultati del secondo modulo.

-- SimoneSilvestri - 04 Jun 2008

---

Re: solver_analyze

potreste considerare una lieve variazione del prototipo della funzione ...

-- FrancescoParisiPresicce - 06 Jun 2008

---

nof_conflitti e nof_learnts

Non ho ben capito se dobbiamo gestire, oltre al caso che il numero dei conflitti diventi maggiore di nof_conflitti (e torniamo undef), anche quello in cui il numero di clausole apprese superi la somma tra il numero di assegnamenti e nof_learnts, come ha scritto in un post sul forum del Modulo 2.

Dalle specifiche mi sembra di capire che dobbiamo escludere questo caso, pero' vorrei averne conferma, se possibile

-- FabioTicconi - 07 Jun 2008

---

Gestire l'output con la test_modulo2() ?

Come da oggetto: dovremmo gestire l'output con la stessa funzione, oppure dobbiamo aggiungere qualcosa nel main che agisca sul ritorno della solver_solve()?

Grazie

-- FabioTicconi - 07 Jun 2008

---

Re: nof_conflitti e nof_learnts

NON va gestito il caso in cui il numero di clausole imparate superi il limite posto da nof_learnts (per semplificare il progetto, non abbiamo gestito l'aggiornamento di alcuni parametri delle variabili e delle clausole). Va invece 'azzerato tutto' nel caso in cui si superi il limite dei conflitti.

-- FrancescoParisiPresicce - 10 Jun 2008

---

Re: Gestire l'output con la test_modulo2() ?

Vedere la pagina del corso di Laboratorio per i dettagli sulla formattazione dell'output del modulo 3

-- FrancescoParisiPresicce - 10 Jun 2008

---

Lucidi Modulo3

Salve, è possibile avere i lucidi utilizzati nell'ultima lezione di Laboratorio di programmazione, i quali contengono uno pseudocodice delle funzioni da implementare nel Modulo3? Grazie in anticipo

-- LauraDiSaverio - 10 Jun 2008

---

Clausole contradditorie

Per i file che contengono due clausole unitarie in evidente contraddizione, come x AND (NOT x), quando viene trovato un conflitto e chiamata la solver_analyze() questa rimuoverà il letterale x in tutte e due le forme, sia dalla clausola di conflitto che dalla clausola ragione del suo inserimento. Il letterale però era l'unico elemento di entrambe le clausole: rimuovendolo, la funzione impara una clausola vuota. A questo punto mi chiedo: il solver potrà ripetere lo stesso percorso? In caso di insoddisfacibilità, quando dovremmo interrompere del tutto la ricerca e segnalare che la proposizione è una contraddizione? grazie

-- DanieleCocca - 11 Jun 2008

---

formattazione output -- chiarimenti ulteriori

Salve, il documento sull'output e' quasi del tutto chiaro, ho solo un paio di dubbi (che sono anche strutturali, credo).

e' possibile che un letterale abbia una stessa wlist ripetuta piu' volte? O prima di aggiungerle, nel programma, devo controllare che non ne esista gia' una uguale?

In OGNI caso devo sempre stampare \n per tutti i letterali (anche non presenti..)? l'esempio e' in allegato.

qui le variabili sono 4 (1, 2, 3, 4), i letterali 5 (1, 2, -2, 3, -4), la grandezza della wlist invece e' 8 (2 * 4):

per -1 e 4 non esisteranno ovviamente wlist, quando andro' a stampare pero' mi posso regolare solo con un ciclo 2*nof_var volte, quindi stampera' "\n" anche alla seconda posizione (-1) e alla 7 (4)..

e' corretto?

Grazie

p cnf 4 3
1 2 0
-2 3 0
1 -2 -4 0

-- FabioTicconi - 12 Jun 2008

---

Formule trivialmente insoddisfacibili

Per quanto riguarda questo tipo di formule, sono state gia' date alcune risposte...

non mi e' ancora pero' perfettamente chiaro se dobbiamo intercettarle nel main, controllando "stato" (il ritorno del main_modulo3), e poi passare lo stato e il solver "incompleto" a test_modulo3() (quindi una sfilza di U nell'assigns, wlist quasi vuote e clausola di conflitto non presente, da specifiche dell'output), oppure se dobbiamo farlo comunque analizzare a solver_analyze.

Grazie

-- FabioTicconi - 12 Jun 2008

---

Aiuto comprensione specifiche

Alla fine delle specifiche del Terzo Modulo, c'e' scritto questo:

"settando ad UNDEF (e ricordandosi di aggiornarne il corrispondente reasons, level ecc. ) tutte le variabili presenti nel trail fino a lev, e si inserisce il letterale corrispondente in coda. La coda non è più vuota, e si ricomincia con la propagazione."

non capisco quale letterale si intenda: dobbiamo inserire in coda il letterale dell'ultima posizione di trail (ricavandolo tramite la variabile in trail e il corrispondente vettore assign), oppure il primo letterale della nuova clausola imparata?

Grazie

-- FabioTicconi - 12 Jun 2008

---

Re: Lucidi Modulo3

Ho mandato una mail al professore, ma e' fuori Roma...mi ha consigliato di chiedere a qualcuno di quelli che frequenta se hanno preso appunti:

ai FREQUENTANTI...potreste postare qui qualche appunto (almeno sullo pseudocodice) riguardante il modulo 3? Fareste un favore immenso a chi non puo' seguire le lezioni per lavoro o altri motivi...

Grazie!!

-- FabioTicconi - 14 Jun 2008

---

Risultati Primo e Secondo Modulo

Sono disponibili le correzioni dei modulo 1 e 2 inviati con il terzo.

Primo modulo:

http://www.dsi.uniroma1.it/~parisi/handouts/risultati_mod_1.html

Secondo modulo:

http://www.dsi.uniroma1.it/~parisi/handouts/tabella_mod_2.html

-- SimoneSilvestri - 16 Jun 2008

---

Comprensione solver_analyze

Ci sono un po' di cose che non mi sono chiare nello pseudocodice della funzione solver_analyze:

1. E' sicuro che i letterali q della clausola di conflitto siano tutti stati settati per scelte aleatorie? Chi ce lo assicura? Se non e' cosi' quale e' il livello di decisione ( LD(q) ), di una variabile che nn e' stata scelta a caso e quindi non si trova in trail_lim???

2. Lo pseudocodice dice:

...se q non e' visto, settiamolo come visto

"- se LD(q) = LD attuale allora counter++

- altrimenti ...."

cio' che ho messo tra virgolette bisogna eseguirlo anche se q e' gia' stata vista??

3. Che cosa vuol dire "selezionamo il prossimo letterale da trattare tra quelli non visti in trail"? Bisogna metterlo al posto di p? Se no, dove lo memorizziamo, e quando ci serve? E in che modo lo cerchiamo? Dobbiamo trovare il primo letterale in trail che non compaia in confl? E come ci calcoliamo l'assegnamento del vettore ragione se non abbiamo la clausola di conflitto della nuova variabile?

-- ClaudiaRapuano - 19 Jun 2008

---

No such template def TMPL:DEF{PROMPT:thread}