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 }
La variabile che appare più volte in clausole binarie è la d (tre volte). Si fa quindi branching su questa variabile, cominciando con il valore negativo dato che -d compare due volte in clausole binarie mentre d una volta sola.
La propagazione unitaria di d=0 produce i seguenti cambiamenti:
{ ¬ 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} =
{ ¬ b ∨ c, ¬ a ∨ b, ¬ e ∨ f, ¬ b ∨ ¬ c ∨ f, a ∨ b ∨ e ∨ f, a ∨ c ∨ ¬ e, a ∨ b ∨ ¬ e, ¬ c ∨ ¬ e ∨ ¬ f, ¬ b ∨ ¬ f, a }
La propagazione di a genera:
{ ¬ b ∨ c,¬ a∨ b, ¬ e ∨ f, ¬ b ∨ ¬ c ∨ f,a ∨ b ∨ e ∨ f,a ∨ c ∨ ¬ e,a ∨ b ∨ ¬ e, ¬ c ∨ ¬ e ∨ ¬ f, ¬ b ∨ ¬ f } =
{ ¬ b ∨ c, b, ¬ e ∨ f, ¬ b ∨ ¬ c ∨ f, ¬ c ∨ ¬ e ∨ ¬ f, ¬ b ∨ ¬ f }
Qui e appare solo negativa, per cui si potrebbe anche usare la regola dei letterali puri. Si può anche eseguire la propagazione il più possibile, e solo dopo procedere con i letterali puri, cosa che si è scelto di fare in questo caso (non è comunque considerato un errore applicare invece la regola dei letterali puri). La propagazione di b genera:
{¬ b∨ c, ¬ e ∨ f,¬ b∨ ¬ c ∨ f, ¬ c ∨ ¬ e ∨ ¬ f,¬ b∨ ¬ f } =
{ c, ¬ e ∨ f, ¬ c ∨ f, ¬ c ∨ ¬ e ∨ ¬ f, ¬ f }
La propagazione di c ora genera f, che però appare già negata nell'insieme. Si ottiene quindi una inconsistenza.
Si prova ora il valore d=1. La propagazione unitaria produce il seguente risultato.
{¬ 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 } =
{ e ∨ f, ¬ b ∨ ¬ c ∨ f, a ∨ b ∨ e ∨ f, a ∨ c ∨ ¬ e, a ∨ b ∨ ¬ e, ¬ c ∨ ¬ e ∨ ¬ f, b ∨ ¬ f, ¬ b ∨ ¬ f, ¬ a, c }
La propagazione di ¬ a e di c genera:
{ e ∨ f, ¬ b ∨¬ c∨ f,a∨ b ∨ e ∨ f,a ∨ c ∨ ¬ e,a∨ b ∨ ¬ e,¬ c∨ ¬ e ∨ ¬ f, b ∨ ¬ f, ¬ b ∨ ¬ f } =
{ e ∨ f, ¬ b ∨ f, b ∨ e ∨ f, b ∨ ¬ e, ¬ e ∨ ¬ f, b ∨ ¬ f, ¬ b ∨ ¬ f }
Nessun letterale appare negativo o con un solo segno. Si procede quindi alla scelta di una nuova variabile e di un nuovo valore. Dato che f compare cinque volte in clausole binarie, mentre le altre variabili meno (b: quattro volte, e: tre volte), si sceglie questa variabile. Dato che f compare tre volte negativa e due positiva, si prova prima il valore negativo.
La propagazione di ¬ f genera:
{ e ∨f, ¬ b ∨f, b ∨ e ∨f, b ∨ ¬ e,¬ e ∨ ¬ f, b ∨ ¬ f,¬ b ∨ ¬ f} =
{ e, ¬ b, b ∨ e, b ∨ ¬ e, b ∨ ¬ f }
La propagazione di ¬ b produce ¬ e e quindi una inconsistenza.
La propagazione di f genera:
{e ∨ f,¬ b ∨ f,b ∨ e ∨ f, b ∨ ¬ e, ¬ e ∨¬ f, b ∨¬ f, ¬ b ∨¬ f} =
{ b ∨ ¬ e, ¬ e, b, ¬ b }
Si ottiene quindi una inconsistenza.
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) }
Questo è un possibile tableau che dimostra la insoddisfacibilità dell'insieme. Le formule ¬ P(a,a) e ∃ x ¬ Q(x) in basso a destra sono ottenute per applicazione della regola dell'or dalla formula ¬ P(a,a) ∨ ∃ x ¬ Q(x) che si trova nella terza riga.
Eseguire l'algoritmo AC-3 sul seguente problema di vincoli. Mostrare come cambiano i singoli domini ad ogni passo.
Sia D l'insieme dei vincoli da considerare. Inizialmente questo insieme contiene tutti i vincoli.
Notare che l'algoritmo non prosegue oltre: appena anche un singolo dominio resta vuoto, ci si ferma e si conclude che il problema non ha soluzioni.