Compito esame ragionamento automatico
Quarto appello 2007

Domanda 1

Eseguire l'algoritmo di Davis-Putnam (DPLL) sul seguente insieme, e dire se è o meno soddisfacibile. Mostrare l'albero di ricerca, evidenziando in ogni nodo i letterali che si ottengono per propagazione unitaria e uso dei letterali puri.

{ ¬ b ∨ c ∨ d, e ∨ ¬ d ∨ f, ¬ a ∨ b ∨ d, ¬ e ∨ d ∨ f, ¬ b ∨ ¬ c ∨ f, a ∨ b ∨ e ∨ f, a ∨ c ∨ ¬ e,
a ∨ b ∨ ¬ e, ¬ c ∨ ¬ e ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, ¬ b ∨ ¬ f, a ∨ d, ¬ a ∨ ¬ d, ¬ d ∨ c }

Domanda 2

Verificare se il seguente insieme è soddisfacibile o meno usando il metodo dei tableaux. In caso di soddisfacibilità, indicare come è fatto un modello.

{ ∀ x P(x,x), ∀ x &forall y (P(x,x) → Q(y)), ¬ P(a,a) ∨ ∃ x ¬ Q(x) }

Domanda 3

Eseguire l'algoritmo AC-3 sul seguente problema di vincoli. Mostrare come cambiano i singoli domini ad ogni passo.

variabili:
x, y, z
dominii:
Dx = Dy = Dz = {1, 2, 3}
vincoli:
x = y, y<z, z<x