Tags:
create new tag
view all tags
---++ Domande sul Modulo Due * Aggiungete le vostre domande in [[#InFondo][fondo alla pagina]] %TOC% --- ---+++ letterali e stack quando si parla di variabile+valore cosa significa di preciso? essendo il letterale un intero, come memorizzo entrambe le informazioni? inoltre non ho capito come devono essere interpretate trail e trail_lim, ossia cosa contengono di preciso? <verbatim> </verbatim> -- %MAINWEB%.FabioDiBenedetto - 22 Apr 2008 --- ---+++ Classe CodaStack Nelle specifiche del modulo II si dice di creare una classe CodaStack() con una serie di metodi per gestire code e stack. Il fatto che all'interno del solver le variabili PCoda, trail e trail_lim sono definite di tipo vec_i suggerisce chiaramente che per le code e lo stack si deve dare una implementazione con vettori. La mia domanda è se non sia più sensato implementare la coda PCoda come una lista linkata piuttosto che con un array... <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 25 Apr 2008 --- ---++++ Re: Classe CodaStack Per questo tipo di problema, la velocita' di esecuzione e' piu' importante del risparmio di spazio in memoria <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 25 Apr 2008 --- ---++++ Re: letterali e stack trail contiene la lista delle variabili cui e' stato assegnato valore TRUE o FALSE, nell'ordine in cui e' stato assegnato. Trattata come pila (prima ad essere rimossa e' l'ultima variabile assegnata) per il backtracking, necessario dopo aver scoperto che l'assegnamento corrente produce una contraddizione. trail_lim contiene l'informazione (indice) di dove finisce un livello e ne comincia un altro. Serve per sapere fino a che punto tornare indietro : se si sceglie un valore da assegnare a x4, e questo costringe un preciso valore di x9 e x2 perche' crea clausole unitarie, allora x4, x9 e x2 (inserite in quet'ordine in trail) hanno lo stesso livello ed un successivo backtracking dovra' annullare il valore di tutte e tre queste variabili o di nessuna delle tre. <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 25 Apr 2008 --- ---+++ Problemi di cross-referencing Nelle nuove specifiche si deve modificare la new_clause() e in particolare si deve aggiungere un parametro di tipo puntatore a solver. E' anche vero, però, che le funzioni del solver(solver.h e solver.c) fanno riferimento alla struttura clause. Ad occhio(non ho ancora provato a implementare il tutto) in questo modo si viene a determinare una situazione di cross-referencing tra solver.h e clause.h. Questo problema si può risolvere con noti "trucchi sporchi" ma mi chiedo se non sia meglio, a livello logico, spezzare new_clause(che vorrebbe essere una specie di costruttore) in due funzioni logicamente e fisicamente separate: #include "clause.h" /* * Semplifica la clausola passata e la posizione in c. * Se è presente un letteale e la sua negazione restituisce true. */ bool new_clause(bool appr, float act, vec_i *v, clause *c); #include "solver.h" /* * Se la clausola passata è unitaria, essa viene aggiunta nella * coda dei letterai da propagare. * Altrimenti aggiunge la clausola nella WL solo della negazione * dei primi due letterali. */ void solver_init_clause(solver *s, clause *c); <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 26 Apr 2008 --- ---++++ Re: Problemi di cross-referencing Mi scuso, twiki ha formattato nel modo peggiore possibile l'ultima parte del mio messaggio. Vediamo se allegnado il codice il sistema mantiene una formattazione decente... <verbatim> #include "clause.h" /* * Semplifica la clausola passata e la posizione in c. * Se è presente un letteale e la sua negazione restituisce true. */ bool new_clause(bool appr, float act, vec_i *v, clause *c); #include "solver.h" /* * Se la clausola passata è unitaria, essa viene aggiunta nella * coda dei letterai da propagare. * Altrimenti aggiunge la clausola nella WL solo della negazione * dei primi due letterali. */ void solver_init_clause(solver *s, clause *c); </verbatim> -- %MAINWEB%.DonatoCapitella - 26 Apr 2008 --- ---+++ solver nof_conflitti e nof_learnts sono variabili da aggiungere alla struttura solver??? Perchè inizialmente settati rispettivamente a 100 e al numero totali di clausole diviso 3???? e perchè....Ad ogni iterazione in cui solve_search restituisce UNDEF tali parametri vanno moltiplicati rispettivamente per 1.1 e dell 1.5 dei valori precedenti??? <verbatim> </verbatim> -- %MAINWEB%.GiuliaChelli - 28 Apr 2008 --- ---+++ RISULTATI PRIMO MODULO All'indirizzo: http://www.dsi.uniroma1.it/~parisi/handouts/risultati1.html sono disponibili i risultati relativi alla correzione del primo modulo. <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 28 Apr 2008 --- ---+++ clause_propagate Ho un pò di problemini nella comprensione delle specifiche del metodo clause_propagate. Qui c'è scritto: ...Il metodo per prima cosa "sposta" "se necessario" il letterale in input nella "seconda posizione" della clausola... Che si intende per "sposta"? Vuol dire che il letterale in seconda posizione prende il posto in cui si trova il letterale in input nella clausola e viceversa? E se il letterale in input compare più volte nella clausola?? In oltre che significa "se necessario"? Quando non è necessario? Come me ne accorgo? Poi segue: ...Se il letterale non è soddisfatto, cerca il primo letterale (escluso il primo) che non è stato assegnato (UNDEF) o che ha valore TRUE e lo intercambia con il letterale in input (che si trova in prima posizione)... Come???? Prima c'era scritto che lo scambiava con quello in seconda posizione!!! Dove va messo questo letterale in prima o in seconda posizione???? <verbatim> </verbatim> -- %MAINWEB%.ClaudiaRapuano - 01 May 2008 --- ---++++ Re: clause_propagate mi associo anche io, non ho capito cosa debba fare questa funzione <verbatim> </verbatim> -- %MAINWEB%.TizianoCialfi - 02 May 2008 --- ---+++ RE: clause_propagate ragazzi, se siete arrivati a clause_propagate() vuol dire che in qualche modo avete risolto il problema di clausole.h e solver.h che ri referenziano a vicenda? <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 02 May 2008 --- ---+++++ Re: Re: clause_propagate Qui c'è scritto: ...Il metodo per prima cosa "sposta" "se necessario" il letterale in input nella "seconda posizione" della clausola... Che si intende per "sposta"? Vuol dire che il letterale in seconda posizione prende il posto in cui si trova il letterale in input nella clausola e viceversa? * SI, esattamente. Si sta propagando il valore TRUE del letterale p e si vuole not(p) in seconda, non prima posizione. se il letterale in input compare più volte nella clausola?? * NO, la clausola dovrebbe essere semplificata e quindi non contenere occorrenze multiple dello stesso letterale. In oltre che significa "se necessario"? Quando non è necessario? Come me ne accorgo? * Se not(p) si trova in prima posizione, va scambiato con quello in seconda Poi segue: ...Se il letterale non è soddisfatto, cerca il primo letterale (escluso il primo) che non è stato assegnato (UNDEF) o che ha valore TRUE e lo intercambia con il letterale in input (che si trova in prima posizione)... * Se il letterale in prima posizione è TRUE, la clausola è soddisfatta. Altrimenti, cerca il primo letterale (dalla posizione 2 in poi) con valore UNDEF o TRUE e scambialo con not(p), che ora si trova comunque in seconda posizione (indice 1) Come???? Prima c'era scritto che lo scambiava con quello in seconda posizione!!! Dove va messo questo letterale in prima o in seconda posizione???? <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 02 May 2008 --- ---+++ CodeStack Ma possiamo definire un nuovo tipo Coda oppure dobbiamo necessariamente usare il tipo vec_p? (per gestire una coda sarebbe comodo avere dei campi nella struttura... fine... inizio :D ) <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 02 May 2008 --- ---++++ Re: CodeStack L'importante è che nel .h ci siano le funzioni come da specifica. vec_i may work better <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 02 May 2008 --- ---++++++ Re: Re: Re: clause_propagate al problema del cross referencing abbiamo momentaneamente risolto con "soluzioni sporche" come da te già scritto, in attesa di ulteriori informazioni. Il problema è che ora siamo a fermi, cercando di capire clause_propagate. <verbatim> </verbatim> -- %MAINWEB%.TizianoCialfi - 03 May 2008 --- ---++++++ Re: Re: Re: clause_propagate Anche io a questo punto penso di risolvere con soluzioni sporche... mi chiedo se non sia il caso di posticipare la consegna in modo da poter parlare di questi problemi a lezione col professore... <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 03 May 2008 --- ---++++++ Re: Re: Re: clause_propagate Sono d'accordo con te. Comunque, ora che ti concentri su clause_propagate, se trovi intoppi ci scambiamo suggerimenti <verbatim> </verbatim> -- %MAINWEB%.TizianoCialfi - 04 May 2008 --- ---+++ Chiarimenti : Typedef int lit Nell prototipo delle funzioni solver_enqueue e clause_propagate, c'è il parametro Lit, il quale è stato definito come intero. Nelle specifiche nella definizione della solver_enqueue c'è scritto che lit rappresenta un letterale (variabile + valore). come è possibile che rappresenti due informazioni se è un intero? <verbatim> </verbatim> -- %MAINWEB%.EmanueleCuozzo - 04 May 2008 --- ---++++ Re: Chiarimenti : Typedef int lit Provo a dare la mia interpretazione... se lit è positivo rappresenta un valore true per il letterale, flase se negativo... può essere? <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 04 May 2008 --- ---+++ valore restituito da new_clause() Se new_clause() deve aggiungere una clausola unitaria alla coda dei letterali da propagare, chiama la solver_enqueue(). Se è già presente un assegnamento per quel letterale che va in contrazzione con l'assegnamento corrente, solver_enqueue() restituisce False. Dobbiamo quindi modificare new_clause in modo che anche questa funzione restituisca False in caso di contraddizione? Quindi dobbiamo modificare anche il main_modulo1()? La situazione a cui mi riferisco è la presenza di due clausole unitarie nel file di ingresso di questo tipo: 1 0 -1 0 spero di essere stato chiaro... si sa qualcosa sulla consegna? Avete deciso di proporagla in modo da poter approfondire alcuni problemi a lezione? <verbatim> </verbatim> -- %MAINWEB%.DonatoCapitella - 04 May 2008 --- ---+++ SLIDE LEZIONE 30-04 Essendo momentaneamente impossibilitato a mettere le slide della lezione del 30-04 online, chi fosse interessato può richiederle via email. saluti, Simone Silvestri <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 05 May 2008 --- ---+++ domande su slide riporto un pezzo dello psudocodice delle slide mostrate a lezione: Funzione: clause_propagate() bool clause_propagate( solver *s , lit x, clause c) { if ( ∃y∈c t.c. assigns[y] = TRUE ) return TRUE; //cosa vuol dire? che assigns[|y|] deve aver valore TRUE o che nella clausola il valore di y sia TRUE (cioè per y>0 => assigns[y] = TRUE, per y<0 => assigns[|y|] = FALSE)? if ( |x| = TRUE ) return TRUE //stessa domanda di prima per x else { trova y∈c t.c. assigns[y] = TRUE or assigns[y] = UNDEF //perchè si ripete il controllo "trova y∈c t.c. assigns[y] = TRUE" se è già stato fatto prima e nel caso fosse risulato vero saremmo già usciti dalla funzione? //altra domanda, nell dispense c'è scritto che X va spostato al secondo posto ma da questo pseudocodice non risulta... seguiamo le indicazioni di questa slide oppure dobbiamo spostare X al secondo posto? //e in quest'ultimo caso x va spostato al secondo posto in tutti i casi in cui non sia già al secondo posto oppure solo se sta al primo? <verbatim> </verbatim> -- %MAINWEB%.ManueleTamburrano - 05 May 2008 --- ---+++ Pseudocodice solver_search Nello pseudocodice come prima cosa controlliamo se abbiamo assegnato un valore a tutti i letterali, in caso affermativo usciamo ritornado True: ossia abbiamo trovato una soluzione valida. Ma non ci possono essere casi in cui, anche se abbiamo assegnato tutti i valori, questi creano un conflitto e la soluzione quindi non e' valida(e quindi dovrei ritornare false)? Non sarebbe meglio svuotare la Pcoda tramite solver_propagate, prima di ritornare True, in modo da vedere se vengono generati conflitti? Ad esempio: clausole: 1 2 -3 3 -2 Inseriro' 1 2 -3 nella Pcoda, e assegnero' i valori di verita' ad assigns, direttamente dalla new_clause, perche' clausole unitarie. La solver_search restituira' True, senza fare ulteriori controlli, ma la formula non ammette soluzione. <verbatim> </verbatim> -- %MAINWEB%.DiegoCarrea - 13 May 2008 --- ---++++ Re: Pseudocodice solver_search Correzione esempio clausole: <verbatim> 1 2 -3 -3 -2 </verbatim> -- %MAINWEB%.DiegoCarrea - 13 May 2008 --- ---+++++ Re: Re: Pseudocodice solver_search Scusate, ulteriore correzione: <verbatim> 1 2 -3 3 -2 </verbatim> -- %MAINWEB%.DiegoCarrea - 13 May 2008 --- ---+++ SU CODESTACK?? è possibile che trail possa essere di tipo vec_i(come trail_lim e Pcoda) invece che lit*?? vi prego di rispondermi al più presto <verbatim> </verbatim> -- %MAINWEB%.DavideDELLAVALLE - 13 May 2008 --- ---+++ WL come stack Se, come consigliato, implemento le WL come stack, credo ci sia un problema in solver_propagate e clause_propagate. Mi sembra di aver capito che in solver_propagate bisogna prelevare una clausola alla volta dalla testa della WL, e passarla a clause_propagate. In alcuni casi, ad esempio quando il letterale in prima posizione ha valore True, la clausola va reinserita, dalla clause_propagate, nella WL. Trattando la WL come stack, la reinserisco in testa. Non si crea quindi un loop? <verbatim> </verbatim> -- %MAINWEB%.FrancescoBrandozzi - 16 May 2008 --- ---++++ Re: SU CODESTACK?? E' proprio quello che mi stavo chiedendo anche io :| Come avete risolto voi per caso? <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 17 May 2008 --- ---++++ Re: Chiarimenti : Typedef int lit io credo che, come dicono le dispense "trail.pdf", il valore sia in lbool *assigns, trail e' solo l'indice della variabile... <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 17 May 2008 --- ---++++ Re: Chiarimenti : Typedef int lit Per letterale si dovrebbe intendere indice variabile + valore, e per valore si intende se negata o meno. Quindi la variabile 5 e -5 sono la stessa variabile, il letterale 5 e -5 sono letterali diversi. Il valore TRUE o FALSE della variabile lo trovate sempre nel campo assigns del solver. Edit: Leggendo le specifiche della funzione solver_enqueue c'è scritto che questa deve aggiornare il vettore assigns, ma allora significa che è qui che il valore True o False del letterale viene messo nel vettore assigns (non nella funzione solver_select quindi) e a questo punto l'unica interpretazione possibile è che se lit è positivo rappresenta un valore True per il letterale, False se negativo... <verbatim> </verbatim> -- %MAINWEB%.RiccardoAmbrosiDeMagistris - 18 May 2008 --- ---+++ solver_select Nelle specifiche non viene descritta precisamente la funzione solver_select, ovvero in che modo seleziona la variabile ed il valore da assegnarle. Il campo int seed del solver viene inizializzato da input e serve a "generare aleatoriamente un indice di variabile nel metodo solver_select". Questo lascia intendere che bisogna usare la funzione rand() in loop finkè non esce una variabile non ancora assegnata, ma così facendo come ci assicuriamo che tramite questo metodo riusciamo a selezionare tutte le variabili non ancora assegnate). Non sarebbe più efficiente scandire il vettore assigns iterativamente finkè non si trova una variabile non assegnata? Resta comunque imprecisato in che modo viene scelto il valore da assegnarle! <verbatim> </verbatim> -- %MAINWEB%.RiccardoAmbrosiDeMagistris - 18 May 2008 --- ---++++ Re: WL come stack Dove avete letto che le WL vanno implementate come stack? <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 19 May 2008 --- ---+++++ Re: Re: WL come stack Nella spiegazione di new clause: "Se la clauola non è unitaria, allora la clausola va aggiunta nella WL solo della negazione dei suoi due primi letterali (anche le WL possono essere tratttate come stack, si veda la sezione Classe Code e Stack)." <verbatim> </verbatim> -- %MAINWEB%.FrancescoBrandozzi - 19 May 2008 --- ---++++ Re: Re: Chiarimenti : Typedef int lit Secondo le specifiche, solver_select inserisce il letterale cui assegnare il valore TRUE nella coda per essere propagato. Il metodo solver_enqueque aggiorna assigns. <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 19 May 2008 --- ---++++ Re: solver_select Nelle specifiche non viene descritta precisamente la funzione solver_select, ovvero in che modo seleziona la variabile ed il valore da assegnarle. ** questa e' una semplificazione. In pratica, altri fattori intervengono per selezionare il letterale successivo quando la coda e' vuota Il campo int seed del solver viene inizializzato da input e serve a "generare aleatoriamente un indice di variabile nel metodo solver_select". Questo lascia intendere che bisogna usare la funzione rand() in loop finkè non esce una variabile non ancora assegnata, ma così facendo come ci assicuriamo che tramite questo metodo riusciamo a selezionare tutte le variabili non ancora assegnate). Non sarebbe più efficiente scandire il vettore assigns iterativamente finkè non si trova una variabile non assegnata? ** si potrebbe usare il valore aleatorio per stabilire a che punto iniziare la 'scansione' (e prendere, per esempio, il primo letterale a destra di quello restituito 'aleatoriamente') Resta comunque imprecisato in che modo viene scelto il valore da assegnarle! ** se si sceglie un intero con segno, il valore e' automatico (se, per esempio, la scelta aleatoria restituisce -32, si assegna FALSE alla variabile x32 in quanto -32 viene inserito in coda ed assegnato il valore TRUE ) <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 19 May 2008 --- ---+++ Comprensione solver_search e solver_select Vorrei qualche delucidazione sui metodi solver_search e solver_select: 1.Cosa ritorna la funzione solver_serach nel caso in cui venga chiamata la solver_select? 2. Solver_select restituisce qualcosa? E se sì che cosa? 3. Viene implementato nel modulo 3 il fatto che solver_search restituisce UNDEF quando il nr. di conflitti supera il limite e FALSE quando il livello di decisione è quello della radice? <verbatim> </verbatim> -- %MAINWEB%.ManueleTamburrano - 19 May 2008 --- ---+++ valori Pcoda? Cosa contiene Pcoda? Solamente l'indice delle variabili da propagare (valori assoluti quindi: 32, 4, 5, 2, etc.), o variabile+valore (ad esempio: -32, 4, 5, -2, etc.)? Dalla risposta del professore data qui sopra "...in quanto -32 viene inserito in coda..." sembra che contenga variabile+valore ma dalle specifiche sembra contenga il valore assoluto. Riporto una parte delle specifiche della solver_enqueue: "inserire l'indice del letterale nella Pcoda..." <verbatim> </verbatim> -- %MAINWEB%.ClaudiaRapuano - 20 May 2008 --- ---+++ test_modulo2 Riguarda alla stampa: 1)servono spazi tra i valori di assign? 2)bisogna inserire uno spazio tra virgole che separano le clausole? 3)siccome i letterali di una clausola vanno separati da uno spazio, va bene lasciare uno spazio anche dopo l'ultimo letterale? <verbatim> </verbatim> -- %MAINWEB%.FrancescoBrandozzi - 20 May 2008 --- ---++++ Re: test_modulo2 Rispondo nell'ordine: 1)Si servono spazi, ad esempio: >T F T U T T F 2)no. potete scrivere la virgola subito dopo l'ultimo letterale e scrivere poi il primo della clausola successiva. 3)no, dopo l'ultimo letterale c'è subito \n saluti, Simone Silvestri <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 20 May 2008 --- ---+++ Formule insoddisfacibili e nome dell'eseguibile Nel caso di formule molto semplici come (x AND (NOT x)) che sono riconosciute insoddisfacibili già da main_modulo1() - quando questa restituisce False - lasciamo che venga stampato "Formula\nUNSATISFIABLE\n" o lanciamo test_modulo2()? Dobbiamo anche riadattare il Makefile o lasciamo che generi in output un eseguibile chiamato "modulo1"? <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 20 May 2008 --- ---++++ Re: Formule insoddisfacibili e nome dell'eseguibile -Chiamate test_modulo2() in ogni caso. -Cambiate il make file generando un eseguibile chiamato "modulo2". Per chi consegna sia il modulo 2 che il modulo 1, vi ricordo di fare due cartelle distinte, una che con il modulo1 come per la prima consenga, l'altra con il modulo 2. saluti <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 21 May 2008 --- ---++++ Re: Comprensione solver_search e solver_select 1.Cosa ritorna la funzione solver_serach nel caso in cui venga chiamata la solver_select? ** ancora niente. Dopo solver_select, viene chiamata solver_assume e si aggiunge un letterale nella coda per riprendere la propagazione. 2. Solver_select restituisce qualcosa? E se sì che cosa? **deve restituire un letterale (al quale solver_assume assegna valore TRUE), cioe' variabile e segno 3. Viene implementato nel modulo 3 il fatto che solver_search restituisce UNDEF quando il nr. di conflitti supera il limite e FALSE quando il livello di decisione è quello della radice? **SI/NO nel Modulo3, la funzione viene estesa per restituire UNDEF se il no. di conflitti supera nof_conflict (o no. clausole apprese eccede la somma di no. assegnamenti e nof_learnts) nel Modulo2, deve restituire FALSE se c'e' un conflitto <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 21 May 2008 --- ---++++ Pseudocodice solver_search Mi associo a Diego Carrea, a cui nessuno ha ancora risposto. Riespongo brevemente il problema: Nello pseudocodice fornito dal professore (allegato qui sotto), la solver_search nel caso in cui nel vettore assigns tutte le variabili siano assegnate, ritorna immediatamente TRUE (ovvero riconosce la formula come soddisfacibile) e non chiama ulteriormente la solver_propagate sui rimanenti letterali in PCoda. Pero' non e' detto che questo sia vero, ad esempio nel caso in cui ho le seguenti clausole: (1) (2) (-1 v -2) il vettore assigns sara' riempito durante l'esecuzione delle varie new_clause, quindi quando arriveremo ad eseguire solver_search, essa trovera' tutte le variabili gia' assegnate e tornera' TRUE, ma la formula in realta' non e' soddisfacibile. Non tengo conto delo pseudocodice che e' sbagliato o sono io che non vedo qualcosa? <verbatim> lbool solver_search( solver *s, double nof_conflitti, double nof_learnts){ while (ci sono variabili da assegnare){ if (is_empty(Pcoda)){ lit x = solver_select() solver_assume(s, x) } clause *c = solver_propagate(s) if (c !=NULL) return FALSE } return TRUE } </verbatim> -- %MAINWEB%.ManueleTamburrano - 21 May 2008 --- ---++++ Re: valori Pcoda? Pcoda contiene letterali, cioe' variabili e segno. A questi letterali viene assegnato il valore TRUE (se viene estratto -32, si assegna FALSE alla variabile 32) "inserire l'indice del letterale nella Pcoda..." non dice inserire l'indice della variabile <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 21 May 2008 --- ---++++ Re: Pseudocodice solver_search Dopo la semplificazione della prima clausola (che diventa la clausola unitaria con il solo letterale x2), viene inserito 2 nella Pcoda, poi, solver_enqueue tenta di aggiungere il letterale -2 (in quanto la seconda clausola e' unitaria) e scopre la contraddizione (enqueue verifica, prima dell'aggiunta effettiva, che il letterale con abbia gia' in coda una copia (non si aggiunge) od il suo negato (conflitto!) o non contraddica un assegnamento gia' effettuato) <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 21 May 2008 --- ---++++ Re: Re: Pseudocodice solver_search il mio esempio era formattato male e le clausole sembravano diverse da come le intendevo, il giusto esempio e' questo: (1)(2)(-1 v -2) In questo caso, 1 e 2 saranno inseriti in PCoda e settati come TRUE poiche' sono clausole unitarie (new_clause chiama la solver_enqueue solo su esse), quindi la solver_search in seguito ritornera' subito TRUE perche' tutte le variabili della formula sono state assegnate, ma cio' e' sbagliato poiche' la clausola (-1 v -2) crerebbe conflitto ma nessun letterale viene propagata per potersene accorgere... <verbatim> </verbatim> -- %MAINWEB%.ManueleTamburrano - 21 May 2008 --- ---+++++ Re: Re: Pseudocodice solver_search Mi associo anch'io al problema! E non riesco capire la risposta del professore. Io la vedo cosi': Con una formula del genere (1)(2)(-1 v -2) il programma dovere fare questo: 1. chiama la new_clause() su (1) => clausola unitaria, mette in Pcoda 1, assegna s->assigns[1] = TRUE; 2. chiama la new_clause() su (2) => clausola unitaria, mette in Pcoda 2, assegna s->assigns[2] = TRUE; 3. chiama la new_clause() su (-1 v -2) => mette nella watcher list di 1 e 2 la clausola; 4.chiama solver_search() che chiama la solver_propagate SOLO SE ci sono variabili non assegnate in s->assigns. Quindi nel nostro caso non le chiama e ritorna TRUE, cioe' formula soddisfacibile, quando invece non lo e'. Anche secondo me dovrebbe scandire tutta la Pcoda finche' non e' vuota... Se non e' cosi', cosa c'e' che non capisco? <verbatim> </verbatim> -- %MAINWEB%.ClaudiaRapuano - 21 May 2008 --- ---+++ Possiamo cambiare LIM TRAIL in VECI TRAIL? Il tipo veci e' un vettore di interi con delle informazioni utili a una gestione piu' veloce del vettore...su un veci e' facile costruire un piccolo set di istruzioni per considerarlo come uno stack o una coda. Poiche' trail non e' altro che un vettore di interi, come trail_lim, perche' utilizza un tipo piu' "rozzo" come lim, invece di veci? E' un refuso o e' voluto? <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 22 May 2008 --- ---+++ ATTENZIONE CONSEGNA La nuova data di scadenza per la consegna del Modulo2 è MARTEDI' 27 maggio 2008 alle 20:00 <verbatim> </verbatim> -- %MAINWEB%.FrancescoParisiPresicce - 22 May 2008 --- ---+++ WL come faccio a mettere i letterali nella WL?che funzione utilizzo? <verbatim> </verbatim> -- %MAINWEB%.FabrizioMagliocchetti - 23 May 2008 --- ---++++ Re: WL Credo che tu possa tranquillamente crearti delle funzioni per la gestione delle WL, altrimenti modifichi direttamente watches dove c'e' bisogno (ma ti consiglio la prima ;) ) <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 24 May 2008 --- ---++++ Re: WL Le watcher list contengono per ogni letterale i puntatori alle clausole in cui quel letterale, negato, compare in prima o seconda posizione. che significa quindi Wmettere i letterali nella WL"? Ovviamente si possono creare funzioni ausiliare sia per le WL che per ogni altra struttura dati o funzionalità del progetto in cui sia opportuno. <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 24 May 2008 --- ---++++ Re: WL Puoi farti delle funzioni ausiliarie in modo da semplificare il lavoro, in fondo per la watchlist devi solo prendere l'indice x della variabile (negata) che stai cercando e aggiungere la clausola che ti serve con un vecp_ins(&(s->watches[x]), clausola);. <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 24 May 2008 --- ---+++ Problemi con la coda Continuo ad avere problemi a capire come deve funzionare la coda. Con lo stesso esempio della mia ultima domanda, se io ho l'espressione (x1) AND (NOT x1), il main() chiama main_modulo1() che legge le due clausole e tenta di aggiungerne i letterali. Primo passo: new_clause() riceve x1, chiama solver_enqueue() che non trova alcuna assegnazione per quella variabile (x1=lUndef) e fa quindi il suo dovere, e restituisce True. Secondo passo: new_clause() riceve -x1, chiama solver_enqueue() che trova una diversa assegnazione di x1 già fatta (x1=lTrue) e restituisce False. A questo punto, però, sarà stata aggiunta una sola variabile nella coda del solver (cioè x1) e solver_propagate() assegnerà x1=True. Il problema è che così tutte le variabili saranno state assegnate e la coda si sarà svuotata, e solver_search() terminerà dando per soddisfacibile l'espressione, quando in realtà non lo è. Ho sbagliato l'interpretazione di qualche passo? Grazie. :) <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 24 May 2008 --- ---+++ OUTPUT: Incongruenza nel pdf Nel caso ci sia in conflitto, c'e' una incongruenza su come dobbiamo stampare l'output: nell'esempio, viene stampato: UNSAT (qui l'assegnamento) (qui la clausola di conflitto) (watcher list...) ... ... invece, nella spiegazione sotto, dice che alla riga due ci va la clausola di conflitto, e alla tre gli assegnamenti. quale delle due e' quella giusta? Grazie. <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 25 May 2008 --- ---+++ solver_select: come fare? Non riesco ancora a capire per bene come funzioni la solver_select()... deve utilizzare il vettore assigns? Professore, ci puo' per favore scrivere un piccolo pdf di esempio, o fare un esempio pratico qui? <verbatim> </verbatim> -- %MAINWEB%.FabioTicconi - 25 May 2008 --- ---++++ Re: Problemi con la coda Riprendo il suo esempio. formula: (x1)and(-x1) new_clause chiama solver_enqueue su x1, come dice lei finqui tutto bene. new_clause dopo chiama solver_enqueue su -x1 ma a quel punto solver_enqueue torna false, perchè è si è trovato già quel letterale nella coda con valore di verità opposto. Si è quindi trovato il conflitto. <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 26 May 2008 --- ---++++ Re: OUTPUT: Incongruenza nel pdf fate come riportato nel riquadro. Riga1: La stringa“UNSAT”(maiuscolo!) indicachesiètrovatoun conflitto. Riga2: Stampa dell’assegnamento (vettoreassign). I valori di verità sono rappresentati dalle lettere T (true), F (false), U (undef) Riga3: clausola di conflitto Riga4: Watcher list dituttii letterali. Le clausolesonoseparate davirgole. La rigai-esimacorrispondeall’i-esimaposizionenelvettorewatches. <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 26 May 2008 --- ---++++ Re: Re: Problemi con la coda Sì, logicamente mi ritrovo anche io con la stessa conclusione, ma è per questo che inizialmente ho chiesto se dovevamo in ogni caso chiamare test_modulo2(), perché il fallimento di new_clause() da quanto vedo è intercettato solo nel codice di main_modulo1(), ed eventuali fallimenti nell'aggiunta delle clausole non arriveranno al solver, perché semplicemente con new_clause() non sarà stato aggiunto (-x1) alle assegnazioni o alla coda tramite solver_enqueue(), e non arrivano a test_modulo2(). <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 26 May 2008 --- ---++++ Re: Re: Problemi con la coda Come non detto, credo di aver risolto per ora, temo di aver malinteso un pezzo della della spcifica di new_clause() finora. :) <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 26 May 2008 --- ---+++ RISULTATI SECONDO MODULO All'inidirizzo: http://www.dsi.uniroma1.it/~parisi/handouts/risultati2.html sono disponibili i risultati del secondo modulo. <verbatim> </verbatim> -- %MAINWEB%.SimoneSilvestri - 04 Jun 2008 --- ---+++ Output del solver Ho consegnato il solver in uno stato che gli impediva, purtroppo, di terminare con successo la scansione delle clausole alla ricerca di conflitti. Ora ho corretto il codice e testato il tutto sui cinque file di input elencati nella pagina dei risultati, e il programma _sembra_ funzionare correttamente su tutti gli input. Ci è possibile conoscere, a questo punto, l'output esatto che il solver dovrebbe generare dal modulo2 per confrontarlo con quello che otteniamo? Non sapendo con certezza se il modulo funziona come richiesto, non vorrei lavorare al modulo3 partendo da un modulo2 "apparentemente" funzionante. <verbatim> </verbatim> -- %MAINWEB%.DanieleCocca - 07 Jun 2008 --- %COMMENT{type="thread"}% #InFondo
E
dit
|
A
ttach
|
Watch
|
P
rint version
|
H
istory
: r58
<
r57
<
r56
<
r55
<
r54
|
B
acklinks
|
V
iew topic
|
Ra
w
edit
|
M
ore topic actions
Topic revision: r58 - 2018-11-28
-
AlessandroBasilici
Log In
or
Register
Labprog2/AD Web
Create New Topic
Index
Search
Changes
Notifications
Statistics
Preferences
Prenotazioni esami
Laurea Triennale ...
Laurea Triennale
Algebra
Algoritmi
Introduzione agli algoritmi
Algoritmi 1
Algoritmi 2
Algoritmi per la
visualizzazione
Architetture
Prog. sist. digitali
Architetture 2
Basi di Dati
Basi di Dati 1 Inf.
Basi di Dati 1 T.I.
Basi di Dati (I modulo, A-L)
Basi di Dati (I modulo, M-Z)
Basi di Dati 2
Calcolo
Calcolo differenziale
Calcolo integrale
Calcolo delle Probabilitą
Metodi mat. per l'inf. (ex. Logica)
canale AD
canale PZ
Programmazione
Fond. di Programmazione
Metodologie di Programmazione
Prog. di sistemi multicore
Programmazione 2
AD
EO
PZ
Esercitazioni Prog. 2
Lab. Prog. AD
Lab. Prog. EO
Lab. Prog. 2
Prog. a Oggetti
Reti
Arch. di internet
Lab. di prog. di rete
Programmazione Web
Reti di elaboratori
Sistemi operativi
Sistemi Operativi (12 CFU)
Anni precedenti
Sistemi operativi 1
Sistemi operativi 2
Lab. SO 1
Lab. SO 2
Altri corsi
Automi, Calcolabilitą
e Complessitą
Apprendimento Automatico
Economia Aziendale
Elaborazione Immagini
Fisica 2
Grafica 3D
Informatica Giuridica
Laboratorio di Sistemi Interattivi
Linguaggi di Programmazione 3° anno Matematica
Linguaggi e Compilatori
Sistemi Informativi
Tecniche di Sicurezza dei Sistemi
ACSAI ...
ACSAI
Computer Architectures 1
Programming
Laurea Magistrale ...
Laurea Magistrale
Percorsi di studio
Corsi
Algoritmi Avanzati
Algoritmica
Algoritmi e Strutture Dati
Algoritmi per le reti
Architetture degli elaboratori 3
Architetture avanzate e parallele
Autonomous Networking
Big Data Computing
Business Intelligence
Calcolo Intensivo
Complessitą
Computer Systems and Programming
Concurrent Systems
Crittografia
Elaborazione del Linguaggio Naturale
Estrazione inf. dal web
Fisica 3
Gamification Lab
Information Systems
Ingegneria degli Algoritmi
Interazione Multi Modale
Metodi Formali per il Software
Methods in Computer Science Education: Analysis
Methods in Computer Science Education: Design
Prestazioni dei Sistemi di Rete
Prog. avanzata
Internet of Things
Sistemi Centrali
Reti Wireless
Sistemi Biometrici
Sistemi Distribuiti
Sistemi Informativi Geografici
Sistemi operativi 3
Tecniche di Sicurezza basate sui Linguaggi
Teoria della
Dimostrazione
Verifica del software
Visione artificiale
Attivitą complementari
Biologia Computazionale
Design and development of embedded systems for the Internet of Things
Lego Lab
Logic Programming
Pietre miliari della scienza
Prog. di processori multicore
Sistemi per l'interazione locale e remota
Laboratorio di Cyber-Security
Verifica e Validazione di Software Embedded
Altri Webs ...
Altri Webs
Dottorandi
Commissioni
Comm. Didattica
Comm. Didattica_r
Comm. Dottorato
Comm. Erasmus
Comm. Finanziamenti
Comm. Scientifica
Comm Scientifica_r
Corsi esterni
Sistemi Operativi (Matematica)
Perl e Bioperl
ECDL
Fondamenti 1
(NETTUNO)
Tecniche della Programmazione 1° modulo
(NETTUNO)
Seminars in Artificial Intelligence and Robotics: Natural Language Processing
Informatica generale
Primo canale
Secondo canale
II canale A.A. 10-11
Informatica
Informatica per Statistica
Laboratorio di Strumentazione Elettronica e Informatica
Progetti
Nemo
Quis
Remus
TWiki ...
TWiki
Tutto su TWiki
Users
Main
Sandbox
Home
Site map
AA web
AAP web
ACSAI web
AA2021 web
Programming web
AA2021 web
AN web
ASD web
Algebra web
AL web
AA1112 web
AA1213 web
AA1920 web
AA2021 web
MZ web
AA1112 web
AA1213 web
AA1112 web
AA1314 web
AA1415 web
AA1516 web
AA1617 web
AA1819 web
Old web
Algo_par_dis web
Algoreti web
More...
AD Web
Create New Topic
Index
Search
Changes
Notifications
RSS Feed
Statistics
Preferences
P
View
Raw View
Print version
Find backlinks
History
More topic actions
Edit
Raw edit
Attach file or image
Edit topic preference settings
Set new parent
More topic actions
Account
Log In
Register User
Questo sito usa cookies, usandolo ne accettate la presenza. (
CookiePolicy
)
Torna al
Dipartimento di Informatica
E
dit
A
ttach
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki?
Send feedback