Verificare la soddisfacibilità della seguente formula usando la procedura Davis-Putnam (DPLL). In particolare, mostrare l'albero di ricerca, evidenziando in ogni nodo i letterali che si ottengono per propagazione unitaria e uso dei letterali puri.
{ a ∨ b ∨ ¬ c, ¬ a ∨ d ∨ ¬ c, ¬ a ∨ ¬ b ∨ c, a ∨ ¬ b ∨ ¬ c, ¬ a ∨ ¬ b ∨ ¬ c ∨ ¬ d, c &or d, b &or ¬ d, ¬ b ∨ f, ¬ b ∨ e, a &or b ∨ ¬ f &or ¬ e }
Verificare la soddisfacibilità della seguente formula usando il metodo dei tableaux. Usare a scelta il metodo con o senza unificazione.
{ ∀ x ∃ y (P(x) &or Q(x, y)), ¬ P(a), ∀ x ¬ Q(a, x) }
Mostrare i vari passi che vengono effettuati per forzare la consistenza di arco (arc consistency) sul seguente problema. Ad ogni passo, dire su quale archi e nodi si effettua la propagazione e dire quali valori vengono eliminati.
Viene richiesto l'albero di ricerca. Si fa vedere come questo albero viene costruito. Come primo passo, si riporta l'insieme di partenza:
{ a ∨ b ∨ ¬ c, ¬ a ∨ d ∨ ¬ c, ¬ a ∨ ¬ b ∨ c, a ∨ ¬ b ∨ ¬ c, ¬ a ∨ ¬ b ∨ ¬ c ∨ ¬ d, c &or d, b &or ¬ d, ¬ b ∨ f, ¬ b ∨ e, a &or b ∨ ¬ f &or ¬ e }
Dal momento che b è la variable che si trova nel maggior numero di clausole di lunghezza minore, viene scelta come variabile di branching. Si provano quindi i due valori b=0 e b=1. Dal momento che b appare nella clausole binarie due volte negativa e una positiva, si prova prima il valore 0, che potrebbe più facilmente portare ad un modello.
Per propagazione unitaria da ¬ b, le clausole diventano:
{ a ∨b∨ ¬ c, ¬ a ∨ d ∨ ¬ c,¬ a ∨ ¬ b ∨ c,a ∨ ¬ b ∨ ¬ c,¬ a ∨ ¬ b ∨ ¬ c ∨ ¬ d, c &or d,b&or ¬ d,¬ b ∨ f,¬ b ∨ e, a &orb¬ f &or ¬ e } =
{ a ∨ ¬ c, ¬ a ∨ d ∨ ¬ c, c &or d, ¬ d, a &or ¬ f &or ¬ e }
I letterali ¬ f ed ¬ e sono ora puri (sempre negativi nella formula), per cui si possono assegnare. Per propagazione unitaria da ¬ d si ottiene:
{ a ∨ ¬ c, ¬ a ∨d∨ ¬ c, c &ord}= { a ∨ ¬ c, ¬ a ∨ ¬ c, c }
La propagazione unitaria di c porta a derivare a e ¬ a. Il primo ramo dell'albero sipuò quindi chiudere. Notare che era comunque richiesto di segnare i risultati della propagazione unitaria.
Si passa ora al caso b=1. La propagazione unitaria di b produce:
{a ∨ b ∨ ¬ c, ¬ a ∨ d ∨ ¬ c, ¬ a ∨¬ b∨ c, a ∨¬ b∨ ¬ c, ¬ a ∨¬ b∨ ¬ c ∨ ¬ d, c &or d,b &or ¬ d,¬ b∨ f,¬ b∨ e,a &or b ∨ ¬ f &or ¬ e} =
{ ¬ a ∨ d ∨ ¬ c, ¬ a ∨ c, a ∨ ¬ c, ¬ a ∨ ¬ c ∨ ¬ d, c &or d, f, e }
La propagazione unitaria di f ed e non produce altri letterali, e nessun altro letterale appare solo positivo o solo negativo. Si deve quindi procedere alla scelta di una nuova variable. La variable c è compare tre volte in clausole binarie (due volte positivamente e una negativamente), quindi si sceglie questa variabile, provando prima il valore c=1.
La propagazione di c=1 produce il seguente risultato:
{ ¬ a ∨ d ∨¬ c,¬ a ∨ c,a ∨¬ c, ¬ a ∨¬ c∨ ¬ d,c &or d} = { ¬ a ∨ d, a, ¬ a ∨ ¬ d }
La propagazione unitaria di a produce sia d che ¬ d. Si può quindi chiudere questo ramo.
La propagazione di c=0 produce is seguenti effetti:
{¬ a ∨ d ∨ ¬ c, ¬ a ∨c,a ∨ ¬ c,¬ a ∨ ¬ c ∨ ¬ d,c&or d } = { ¬ a, d }
Dato che tutti i letterali sono ora assegnati e la clausole sono tutte soddisfatte, si è quindi ottenuto un modello della formula di partenza. L'albero risultante è quindi il seguente.
Si inizia mettendo le formule dell'insieme in colonna:
Si è in questo caso scelto di usare la versione con unificazione. Come formula da espandere inizialmente si è scelta la terza (si poteva anche espandere la prima).
A questo punto si può espandere solo la prima formula.
L'unica formula che si può ora espandere è l'ultima.
Anche ora si può solo espandere l'ultima formula.
Il ramo di sinistra chiude con x''=a
A questo punto x'' vale a. Quindi, per chiudere il ramo di destra si può usare x'=f(a)
Si può quindi concludere che l'insieme non è soddisfacibile.
Si supponga di usare l'algoritmo AC3. Inizialmente, tutti i vincoli sono nell'insieme di vincoli potenzialmente non arc-consistenti. Indicando i vincoli con i loro scope, questo insieme contiene quindi inizialmente P={〈x,y〉, 〈y,z〉, 〈z,w〉}.
Si estrae il un elemento, per esempio 〈x,y〉, e si propaga sul vincolo. Questa propagazione non porta a modifiche, per cui si procede con P={〈y,z〉, 〈z,w〉}. Si prende un altro elemento di questo insieme, per esempio 〈y,z〉. La propagazione non produce nessuna modifica nemmeno in questo caso, per cui si procede con P=〈z,w〉}.
In questo caso, la propagazione produce una modifica: i domini di z e w diventano:
A questo punto, in P è stata tolta l'ultima coppia 〈z,w〉, ma vanno rimesse tutte le altre coppie che contengono z e w. In questo caso, l'unica è 〈y,z〉, per cui si continua con P={〈y,z〉}.
Per propagare 〈y,z〉 vanno modificati i domini come segue:
Vengono quindi rimessi in P gli altri vincoli che contengono y. In questo caso P=〈x,y〉.
La propagazione sulla coppia 〈x,y〉 non produce cambiamenti, dato che ogni valore di ogni variable ha un corrispondente nel dominio dell'altra variabile.
A questo punto P è vuoto, per cui la propagazione si arresta. Il risultato sono i seguenti domini: