DomandeModuloDue < Labprog2/AD

Domande sul Modulo Due

Aggiungete le vostre domande in fondo alla pagina

Domande sul Modulo Due

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?

-- 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...

-- 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

-- 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.

-- 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);

-- 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...

#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);

-- 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???

-- 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.

-- 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????

-- ClaudiaRapuano - 01 May 2008

Re: clause_propagate

mi associo anche io, non ho capito cosa debba fare questa funzione

-- 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?

-- 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

* 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????

-- 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 big grin

)

-- DonatoCapitella - 02 May 2008

Re: CodeStack

L'importante è che nel .h ci siano le funzioni come da specifica. vec_i may work better

-- 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.

-- 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...

-- 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

-- 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?

-- 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?

-- 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?

-- 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

-- 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?

-- 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.

-- DiegoCarrea - 13 May 2008

Re: Pseudocodice solver_search

Correzione esempio clausole:

1
2
-3
-3 -2

-- DiegoCarrea - 13 May 2008

Re: Re: Pseudocodice solver_search

Scusate, ulteriore correzione:

-- 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

-- 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?

-- FrancescoBrandozzi - 16 May 2008

Re: SU CODESTACK??

E' proprio quello che mi stavo chiedendo anche io :|

Come avete risolto voi per caso?

-- 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...

-- 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...

-- 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!

-- RiccardoAmbrosiDeMagistris - 18 May 2008

Re: WL come stack

Dove avete letto che le WL vanno implementate come stack?

-- 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)."

-- 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.

-- 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

** 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 )

-- 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?

-- 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..."

-- 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?

-- 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

-- 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"?

-- 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

-- 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

-- 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?

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
}

-- 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

-- 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)

-- 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...

-- 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?

-- 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?

-- FabioTicconi - 22 May 2008

ATTENZIONE CONSEGNA

La nuova data di scadenza per la consegna del Modulo2 è

MARTEDI' 27 maggio 2008 alle 20:00

-- FrancescoParisiPresicce - 22 May 2008

WL

come faccio a mettere i letterali nella WL?che funzione utilizzo?

-- 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 wink

)

-- 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.

-- 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);.

-- 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. smile

-- 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.

-- 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?

-- 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.

-- 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.

-- 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().

-- 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. smile

-- 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.

-- 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.

-- DanieleCocca - 07 Jun 2008

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