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 &or b, ¬ a &or c, ¬ a &or d, a ∨ ¬ b ∨ c ∨ d, ¬ b ∨ ¬ c ∨ ¬ d, a ∨ c ∨ ¬ d, ¬ c ∨ d, ¬ a ∨ c ∨ e ∨ f, ¬ a ∨ b &or ¬ e ∨ ¬ f }
La variable b compare tre volte in clausole binarie, quindi viene scelta come variabile di branching. Dato che compare due volte negata, si sceglie il valore negativo come primo valore da provare.
Gli effetti della propagazione unitaria di ¬ a sono:
{a&or b,¬ a &or c,¬ a &or d,a∨ ¬ b ∨ c ∨ d, ¬ b ∨ ¬ c ∨ ¬ d,a∨ c ∨ ¬ d, ¬ c ∨ d,¬ a ∨ c ∨ e ∨ f,¬ a ∨ b &or ¬ e ∨ ¬ f} =
{ b, ¬ b ∨ c ∨ d, ¬ b ∨ ¬ c ∨ ¬ d, c ∨ ¬ d, ¬ c ∨ d, }
Dalla prima clausola, segue b per propagazione unitaria. La propagazione di questo letterale non produce altri letterali.
{¬ b∨ c ∨ d,¬ b∨ ¬ c ∨ ¬ d, c ∨ ¬ d, ¬ c ∨ d, } =
{ c ∨ d, ¬ c ∨ ¬ d, c ∨ ¬ d, ¬ c ∨ d, }
Come letterale di branching si può ora scegliere indifferentemente c oppure d. In questo caso, si è scelto di usare c. Dato che c appare due volte positiva e due volte negativa, anche la scelta del valore da provare per primo è arbitraria.
Il risultato di imporre c=0 è che vengono generati per propagazione unitaria sia d che ¬ d, e si ha quindi una contraddizione.
Lo stesso si ottiene per propagazione unitaria di c=1.
Avendo ottenuto inconsistenza per a=0, si passa ora all'altro ramo, in cui a=1. Gli effetti della propagazione unitaria sono:
{a &or b,¬ a&or c,¬ a&or d,a ∨ ¬ b ∨ c ∨ d, ¬ b ∨ ¬ c ∨ ¬ d,a ∨ c ∨ ¬ d, ¬ c ∨ d,¬ a∨ c ∨ e ∨ f,¬ a∨ b &or ¬ e ∨ ¬ f } =
{ c, d, ¬ b ∨ ¬ c ∨ ¬ d, ¬ c ∨ d, c ∨ e ∨ f, b &or ¬ e ∨ ¬ f }
Si ottengono quindi c e d. La propagazione di questi due letterali porta al seguente risultato:
{ ¬ b ∨¬ c∨¬ d,¬ c ∨ d,c ∨ e ∨ f, b &or ¬ e ∨ ¬ f } =
{ ¬ b, b &or ¬ e ∨ ¬ f }
Viene quindi anche generato ¬ b. La propagazione unitaria trasforma quindi l'unica altra clausola b &or ¬ e ∨ ¬ f in ¬ e ∨ ¬ f. Dal momento che le variabile e ed f compaiono ora solo negative, si può assegnare loro il valore falso.
Un modello della formula è quindi a, ¬ b, c, d, ¬ e , ¬ f.
Verificare la soddisfacibilità della seguente formula usando il metodo tableaux. Usare a scelta il metodo con o senza unificazione.
{ ∃ x ∀ y Q(x, y), &forall x ¬ Q(a, x), ∀ x (Q(a, x) ∨ ¬ Q(x, x)) }
In questa soluzione si usa il metodo con unificazione. Le prime tre formule sono quelle dell'insieme di partenza. La quarta si ottiene per skolemizzazione della terza. La quindi, sesta e settima sono applicazioni della regola dei quantificatori universali.
Dopo aver applicato la regola dell'or, si ottengono due foglie che chiudono con x''=x'''e con x'''=c e x'=x'''. Un tableau chiuso si sarebbe quindi anche potuto ottenere usando il metodo senza unificazione, usando sempre il valore c per eliminare i quantificatori universali.
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.
Si illustrano i vari passi dell'algoritmo AC3, mostrando lo stato dell'insieme dei vincoli potenzialmente non consistenti e il vincolo che viene preso in considerazione ad ogni passo.
Si ottengono quindi i seguenti domini: