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.
{ a ∨ ¬ b, a ∨ c ∨ d, a ∨ f, b ∨ ¬ c ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, ¬ a ∨ e,
¬ a ∨ c ∨ d, e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨ ¬ e, ¬ c ∨ ¬ d ∨ ¬ e, ¬ a ∨ ¬ c ∨ d ∨ ¬ e, }
Verificare se il seguente insieme è soddisfacibile o meno usando il metodo dei tableaux (B=box, D=diamond). In caso di soddisfacibilità, indicare come è fatto un modello.
{ Bx ∧ Dy, D(¬ x ∨ ¬ y) }
Eseguire l'algoritmo AC-3 sul seguente problema di vincoli. Mostrare come cambiano i singoli domini ad ogni passo.