Compito esame ragionamento automatico
Quinto 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 ∨ ¬ d, ¬ e ∨ ¬ f ∨ ¬ g, a ∨ c ∨ ¬ d ∨ ¬ e, ¬ b ∨ ¬ c ∨ e, c ∨ d ∨ g,
a ∨ ¬ c ∨ f, a ∨ d ∨ f, ¬ a ∨ ¬ b ∨ c, ¬ a ∨ ¬ c, ¬ b ∨ c, b ∨ c ∨ ¬ d ∨ e,
¬ c ∨ ¬ e ∨ ¬ f, ¬ a ∨ b ∨ ¬ e, b ∨ ¬ c ∨ e, c ∨ d ∨ e }

Domanda 2

Verificare se il seguente insieme è soddisfacibile o meno usando il metodo dei tableaux. In caso di soddisfacibilità, indicare come è fatto un modello (ossia, scegliere un dominio come D={1, 2, ...} e poi indicare il valore delle costanti e di P sulle coppie di elementi del dominio).

{ ∃ x ¬ P(x,a), ∃ x ¬ P(a,x), ∀ x P(x,a) ∨ P(a,x) }

Domanda 3

Dire se il seguente problema è arc-consistente e path-consistente. Nel caso di non-consistenza, dire come va modificato per farlo diventare sia arc-consistente che path-consistente.

variabili

{x, y, z}

domini

• D_x={0, 1}
• D_y={0, 1}
• D_z={0, 1}

vincoli

x y 0 0 1 0 1 1

x z 0 0 1 1

y z 1 0 1 1