soluzione mediante traduzione

problema ⇒ soddisfacibilità di una formula booleana ⇒ risolutore

SAT

problema di stabilire se esiste almeno una valutazione delle variabili che rende vera una formula booleana

(a ∨ b) ∧ (¬a ∨ c) ∧ (¬b ∨ c): vera quando a=true, b=false, c=true
a ∧ ¬b ∧ (b ∨ ((¬a ∧ c) ∧ ¬b)): vera quando a=true, b=false, c=true
(¬a ∨ b) ∧ (¬b ∨ c) ∧ a ∧ ¬c: falsa per tutte le valutazioni possibili
equivalente ad a → b, b → c, a, ¬c

prime due sat, terza unsat

problema di pianificazione

insieme di condizioni che possono cambiare nel tempo
loro stato iniziale
loro stato obiettivo, quello che si vuole ottenere
azioni che le modificano

piano = sequenza di azioni per ottenere l'obiettivo

un problema senza piani

condizioni: bottepiena, moglieubriaca
iniziale: bottepiena=true, moglieubriaca=false
obiettivo bottepiena=true, moglieubriaca=true
azioni: bere si può eseguire solo se bottepiena=true effetto: la botte è vuota ma la moglie è ubriaca bottepiena=false, moglieubriaca=true

un problema con un piano

condizioni: bottepiena, moglieubriaca
iniziale: bottepiena=true, moglieubriaca=false
obiettivo bottepiena=true, moglieubriaca=true
azioni: bere si può eseguire solo se bottepiena=true effetto: la botte è vuota ma la moglie è ubriaca bottepiena=false, moglieubriaca=true riempire si può eseguire solo se bottepiena=false effetto: la botte è di nuovo piena bottepiena=true

piano: bere, riempire

problema, in generale

date le condizioni, lo stato iniziale, l'obiettivo e le azioni
esiste un piano per ottenere l'obiettivo?

difficoltà del problema

scala di valutazione: complessità computazionale
dettagli più avanti nel corso

per il momento: problema relativamente difficile

soluzione per riduzione

trova piano ⇒ trova valutazione

riduzione:

trasformare il problema di pianificazione in un equivalente problema di valutazione booleana

trasformazione

le condizioni sono già booleane: bottepiena, moglieubriaca

ma cambiano nel tempo

ipotizzando tre istanti di tempo:
bottepiena potrebbe cambiare in tutti
moglieubriaca anche

variabili della formula booleana

bottepiena₀
bottepiena₁
bottepiena₂
moglieubriaca₀
moglieubriaca₁
moglieubriaca₂

il numero indica il tempo
bottepiena₁ = la botte è piena al tempo 1

stato iniziale

la botte è piena ma la moglie non è ubriaca

bottepiena₀ ∧ ¬moglieubriaca₀

obiettivo

la botte è piena e la moglie è ubriaca

bottepiena₂ ∧ moglieubriaca₂

potrebbe essere vero anche prima

(bottepiena₀ ∧ moglieubriaca₀) ∨ (bottepiena₁ ∧ moglieubriaca₁) ∨ (bottepiena₂ ∧ moglieubriaca₂)

azione `bevi`

rende vero moglieubriaca₁ e falso bottepiena₁

ma solo se è vero bottepiena₀

formula bottepiena₀ → moglieubriaca₁ ∧ ¬bottepiena₁?

no, vorrebbe dire che l'azione è obbligatoria se eseguibile

variabili `bevi_i`

bevi₀
bevi₁

true se si esegue l'azione al tempo 0 o 1

`bevi₀`

bevi₀ → bottepiena₀ ∧ moglieubriaca₁ ∧ ¬bottepiena₁

se si esegue l'azione vuole dire che:

la botte era piena al tempo 0
diventa vuota al tempo 1
e la moglie è ubriaca al tempo 1

`bevi₁`

bevi₁ → bottepiena₁ ∧ moglieubriaca₂ ∧ ¬bottepiena₂

stessa cosa al tempo 1 e 2

`riempi₀` e `riempi₁`

riempi₀ → ¬bottepiena₀ ∧ bottepiena₁
riempi₁ → ¬bottepiena₁ ∧ bottepiena₂

stessa cosa

inerzia

la botte è piena al tempo i se
lo era al tempo i-1
e nessuna azione l'ha svuotata

azioni + inerzia

la botte è piena al tempo i se e solo se
una azione del tempo i-1 l'ha riempita
oppure
era piena al tempo i-1
e nessuna azione l'ha resa falsa

bottepiena₁ ≡ ( riempi₀ ∨ ( bottepiena₀ ∧ ¬bevi₀ ) )

moglie ubriaca

lo stesso
questa volta non ci sono azioni che falsificano

moglieubriaca₁ ≡ ( bevi₀ ∨ ( moglieubriaca₀ ) )

azioni nel secondo passo

stessa formula
indici aumentati

bottepiena₂ ≡ ( riempi₁ ∨ ( bottepiena₁ ∧ ¬bevi₁ ) ) moglieubriaca₂ ≡ ( bevi₁ ∨ ( moglieubriaca₁ ) )

tutto insieme

(bottepiena₀ ∧ ¬moglieubriaca₀) (bottepiena₀ ∧ moglieubriaca₀) ∨ (bottepiena₁ ∧ moglieubriaca₁) ∨ (bottepiena₂ ∧ moglieubriaca₂) bottepiena₁ ≡ ( riempi₀ ∨ ( bottepiena₀ ∧ ¬bevi₀ ) ) moglieubriaca₁ ≡ ( bevi₀ ∨ ( moglieubriaca₀ ) ) bottepiena₂ ≡ ( riempi₁ ∨ ( bottepiena₁ ∧ ¬bevi₁ ) ) moglieubriaca₂ ≡ ( bevi₁ ∨ ( moglieubriaca₁ ) )

devono essere tutte vere
congiunzione

formula soddisfacibile

unico modello:

bottepiena₀=true
moglieubriaca₀=false
bevi₀=true
riempi₀=false
bottepiena₁=false
moglieubriaca₁=true
bevi₁=false
riempi₁=true
bottepiena₂=true
moglieubriaca₂=true

piano: bevi al primo passo, riempi al secondo

formula insoddisfacibile

togliendo l'azione riempi la formula non ha più modelli

nessun piano

altri problemi risolvibili in questo modo

programmazione orari (scheduling)
diagnosi
verifica di sistemi UML
cripoanalisi
verifica software
vincoli SQL
sudoku e altri giochi
…

potenzialmente, qualsiasi problema nella classe di complessità NP
si vedrà più avanti