DomandeModuloTre < Labprog2/EO

Tags: view all tags

---++ Domande sul Modulo Tre
   * Aggiungete le vostre domande in [[#InFondo][fondo alla pagina]]

%TOC%
---

---+++ Riguardo al cambio di livello di decisione...
Supponiamo di avere una formula di 5 variabili e 3 clausole così composta:

(x1 | x2 | x3 | x4) & (x2 | ! x4 | ! x5) & ( ! x4 | x5) 

All'inizio non ci sarà nessuna clausola unitaria, mettiamo il caso che viene selezionata aleatoriamente la variabile x1 ed assegnata al valore True, con relativo passaggio dal livello di decisione iniziale al primo livello di decisione. 
Anche in questo caso non ci sono clausole unitarie; mettiamo che questa volta venga selezionata la variabile x2 e settata a False: si passa dal primo livello di decisione al secondo livello di decisione.
Ancora una volta non ci sono clausole unitarie, mettiamo nuovamente caso che venga selezionata aleatoriamente dal programma la variabile x3 e settata allo stato False, si passa così dal secondo livello al terzo livello di decisione.

Accade ora che la prima clausola abbia tutti i letterali diversi da Undef, meno che uno, cioè x4. x4 però non deve essere settato obbligatoriamente a True per verificare se la formula è soddisfacibile, poiché c'è già il letterale x1 che la rende vera.

Questo vuol dire che pure un ipotetico assegnamento di x4 può far cambiare livello di decisione. Questo è facilmente dimostrabile:

mettiamo, appunto, il caso che la variabile x4 venga selezionata (il livello di decisione diventa il quarto) e settata al valore True: in questo caso la seconda clausola ha tutti i letterali False, meno che !x5 che è ancora Undef, di conseguenza è obbligatorio l'assegnamento della variabile x5 a False. 
In questo caso la terza clausola ha tutti i letterali settati a False, nega tutta la formula e genera un conflitto. 

Dobbiamo quindi tornare al livello di decisione precedente, ovvero il terzo. Mettiamo che anche questa volta venga selezionata aleatoriamente la variabile x4, ma questa volta settata a False; si passa nuovamente al quarto livello di decisione.
In questo caso la prima clausola ha tutti i letterali negati eccetto che x1 che ha valore True (la clausola quindi è True); la seconda clausola ha il letterale !x2 settato a True che la rende True e la terza clausola ha anche essa il letterale !x4 settato a True che la rende True. In questo caso rimane solo la variabile x5 da settare, ma comunque sia il suo valore la formula è soddisfacibile.




Detto questo penso che tutti i letterali all'interno della Pcoda devono esser presi o da clausole che hanno campo size = = 1 o da clausole che hanno tutti i letterali = = False, eccetto uno che deve essere ancora Undef. Per fare ciò potremmo ignorare, nella creazione della Pcoda, le clausole con campo learnts diverso da False, il fatto è che tale campo deve essere selezionato in tutte le clausole in cui occorre un letterale che è appena stato settato a True; notare che tramite il campo watches della struttura solver non è possibile sapere con precisione tutte le clausole dove occorre un certo letterale, poiché ci sono solo clausole dove il letterale occorre esclusivamente in prima od in seconda posizione.
<verbatim>

</verbatim>
-- %MAINWEB%.DarioGangi - 06 Jun 2008
---

---+++ valore back_level
Nella funzione solver_analyze() il valore back_level è inizializzato a 0.
Dalle specifiche tale valore deve essere aggiornato, per i letterali non visti, solo se :

 (il livello di decisione del letterale in esame è diverso dal quello attuale  nel solver) && (il livello di decisione del letterale è > 0).

Questo comporta che se tutti i letterali della ragione sono dello stesso livello di quello del solver, il back_level rimane impostato a 0 e viene restituito come valore di back_level alla solver_search.
La solver_search() esegue una cancellazione di tutti i livello fino al max(back_level, livello iniziale).
Se non ho capito male livello iniziale è s->root_level nel solver, che viene inizializzato a 0 e mai modificato.
Questo comporterebbe come conseguenza, che se tutti i letterali dipendono dall'ultima decisione effettuata (cioè si trovano allo stesso livello di decisione in cui si trova il solver), allora il backtracking verrebbe eseguito fino al livello radice (level = 0).
E' corretta questa analisi o ho trascurato qualcosa di rilevante?
Non sarebbe corretto in questo caso, effettuare un backtracking per modificare semplicemente l'ultima scelta fatta, quindi eliminando solo l'ultimo livello?

Grazie mille



<verbatim>

</verbatim>
-- %MAINWEB%.CristofaroMune - 28 Jun 2008
---
%COMMENT{type="thread"}%
#InFondo