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 }
Nell'insieme, il letterale che appare più volte in clausole binarie è a (tre volte). Dal momento che a appare positiva in due clausole binarie e negata in una, si prova prima il valore a=1.
La propagazione di a=1 ha il seguente effetto:
{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 } =
{ b ∨ ¬ c ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, e, c ∨ d, e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨ ¬ e, ¬ c ∨ ¬ d ∨ ¬ e, ¬ c ∨ d ∨ ¬ e }
Propagando e=1 si ottiene:
{ b ∨ ¬ c ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, c ∨ d,e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨¬ e, ¬ c ∨ ¬ d ∨¬ e, ¬ c ∨ d ∨¬ e} =
{ b ∨ ¬ c ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, c ∨ d, c ∨ ¬ d, ¬ c ∨ ¬ d, ¬ c ∨ d }
Non ci sono altre clausole unitarie. Dal momento che b compare solo positiva ed f solo negativa, la regola dei letterali puri genera b=1 e f=0, e si eliminano tutte le clausole che contengono queste due variabili.
{ c ∨ d, c ∨ ¬ d, ¬ c ∨ ¬ d, ¬ c ∨ d }
Si deve ora scegliere un altro letterale da valutare. Dal momento che sia c che d compaiono in quattro clausole binarie, si può scegliere uno qualsiasi dei due. Dal momento che compaiono due volte positivi e due volte negativi in clausole binarie, si può scegliere prima il valore positivo o il valore negativo. In questo caso, si è scelto di valutare c, usando prima il valore c=0 e poi c=1.
La propagazione di c=0 ha i seguenti effetti.
{c∨ d,c∨ ¬ d,¬ c ∨ ¬ d,¬ c ∨ d}
Si ottengono sia d che ¬ d, generando quindi una contraddizione.
Si passa ora a valutare c=1.
{c ∨ d,c ∨ ¬ d,¬ c∨ ¬ d,¬ c∨ d }
Dato che si ottengono sia d che ¬ d anche in questo caso, si ha una inconsistenza.
Si passa ora a valutare a=0.
{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} =
{ ¬ b, c ∨ d, f, b ∨ ¬ c ∨ ¬ f, b ∨ ¬ d ∨ ¬ f, e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨ ¬ e, ¬ c ∨ ¬ d ∨ ¬ e }
Vengono quindi generati ¬ b e f. La loro propagazione ha i seguenti effetti:
{ c ∨ d,b∨ ¬ c ∨¬ f,b∨ ¬ d ∨¬ f, e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨ ¬ e, ¬ c ∨ ¬ d ∨ ¬ e } =
{ c ∨ d, ¬ c, ¬ d, e ∨ ¬ b ∨ c ∨ d, c ∨ ¬ d ∨ ¬ e, ¬ c ∨ ¬ d ∨ ¬ e }
La propagazione di ¬ c produce d a causa della prima clausola; questo letterale è inconsistente con ¬ d generato in precedenza.
L'albero di ricerca è quindi il seguente:
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.
{ □ x ∧ ◇ y, ◇ (¬ x ∨ ¬ y) }
Il secondo ramo rimane aperto dal momento che in esso sono state applicate tutte le regole applicabili. Gli unici letterali (non modali) di questo ramo sono 1.1 ¬ y e 1.1 x. Un modello è quindi quello in cui c'è un mondo 1 con una interpretazione qualsiasi e un mondo 1.1 con x e ¬ y.
Non è necessario espandere ulteriormente il terzo ramo.
Eseguire l'algoritmo AC-3 sul seguente problema di vincoli. Mostrare come cambiano i singoli domini ad ogni passo.
L'algoritmo AC-3 usa un insieme di vincoli che potrebbero non soddisfare la condizione di arc consistency. Sia P questo insieme. Inizialmente P contiene tutti i vincoli P={x<y, y<z, z<x}. Ad ogni passo viene scelto un vincolo ed estratto da questo insieme.
| vincolo estratto da P | valori che violano la arc consistency |
domini dopo la modifica | nuovo P |
|---|---|---|---|
| x<y | x=2, y=0 | Dx={0,1}, Dy={1,2}, Dx={0,1,2} | P={y<z, z<x} |
| y<z | y=2, z=0, z=1 | Dx={0,1}, Dy={1}, Dx={2} | P={x<y, z<x}
Dy modificato, si rimette x<y perchè contiene y |
| x<y | x=1 | Dx={0}, Dy={1}, Dx={2} | P={z<x} solo Dx modificato a questo passo |
| z<x | x=0, z=2 | Dx={}, Dy={1}, Dx={} | - |
A questo punto ci si ferma dato che il dominio di almeno una variabile è diventato vuoto. Non si prosegue oltre (non è necessario arrivare al punto in cui anche il dominio di y diventa vuoto.