Compito ragionamento automatico
Compito di esempio

Domanda 1

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 }

Domanda 2

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

Domanda 3

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.

variabili
{x, y, z, w}
domini
vincoli

Svolgimento

Domanda 1

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 &or b ¬ 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 &or d }= { 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.

Domanda 2

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.

Domanda 3

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: