10. Risoluzione di problemi per approssimazioni e teorie logiche.

Risoluzione di problemi non difficili

Se un problema non è difficile si può tentare di cercare una formula chiusa che lo risolva senza l'aiuto dell'AI. Se invece il problema è particolarmente difficile possiamo pensare di trasformarlo in qualche altro problema abbastanza studiato, dove quindi si hanno più strumenti risolutivi a disposizione.
Oppure ancora possiamo trasformalo in un problema più semplice rilassando qualche vincolo (come in Ricerca Operativa), ma ciò potrebbe costarci qualcosa in termini di accuratezza ed ottimalità della soluzione trovata nel nuovo problema rispetto al problema originario. Questa strada è quella percorsa dalle euristiche, che spesso trovano, nel problema rilassato, la soluzione esatta del problema originario ma a volte sbagliano e conviene risolvere il problema originario.

Semplificare il problema. Contesto: Teorie logiche

Partiamo dal problema della deduzione rispetto ad una teoria proposizionale. Abbiamo una teoria proposizionale SIGMA ed una frase PHI, vogliamo sapere se $\Sigma \models \varphi$ è vera con la deduzione classica (quella che 'conosciamo' usando modelli ed interpretazioni). Questo è un problema Co-NP completo.

Dubbio: Perchè Co-Np completo? Non dovrebbe essere NP completo? Qui non stiamo cercando la soluzione ad un problema 'negato', bensi al problema diretto, cioè se una data cosa è fattibile.
Cioè capirei fosse Co-NP completo se ci chiedessimo "per caso è possibile dedurre il contrario di phi?". Invece con la deduzione classica andiamo per interpretazioni quindi dobbiamo trovare il modello che renda vera phi e sigma.

Si riesce a trovare una teoria SIGMA' più facile, utile a fare quasi la stessa deduzione ma a costo minore? Questo SIGMA' che caratteristiche deve avere?

  1. $|\Sigma ' | \in P(|\Sigma|)$ . Ovvero SIGMA' deve essere al più polinomialmente grande rispetto a SIGMA (quindi può essere più grande ma non troppo1).
  2. $( \Sigma ' \models \varphi ) \in P{TIME}$. Il costo per stabilire se è possibile o meno la deduzione deve essere polinomiale, cioè appartenere alla classe PTIME.
  3. $\Sigma ' = \Sigma$ . Le due teorie devono essere equivalenti.

Il problema non è tanto verificare le condizioni dato un SIGMA', ma bensì trovare un SIGMA' che rispetti queste condizioni. Se trovare SIGMA' è molto costoso forse conviene risolvere direttamente il problema con SIGMA.

Si dimostra che se esiste un SIGMA' teoria di Horn2 che rispetta il vincolo 3, allora anche gli altri 2 saranno soddisfatti. Purtroppo SIGMA' così fatto non esiste sempre. Si è dimostrato che se SIGMA' esistesse sempre si potrebbero trasformare vari problemi nel problema della deduzione rispetto ad una teoria proposizionale e tutto ciò che è più difficile della classe $\Sigma^P_2$ collasserebbe nella classe di complessità $\Sigma^P_2$.
Allora come si fa visto che SIGMA' non esiste sempre? Si deve rilassare qualche vincolo, ovvero si rinuncia alla corettezza perfetta, quindi al vincolo 3, mantenendo gli altri due vincoli.
Questo approccio è detto Knowledge approximation via Horn compilation.

Concetto di lower bound di Horn

Data una teoria proposizionale $\Sigma$ , la teoria di Horn $\Sigma_{lb}$ è un lower bound di $\Sigma$ se l'insieme dei modelli dell'ipotetico lower bound è contenuto nell'insieme dei modelli della teoria iniziale. Cioè:
$M(\Sigma_{lb}) \subseteq M(\Sigma)$ .

Concetto di upper bound di horn.

Data una teoria proposizionale $\Sigma$ , la teoria di Horn $\Sigma_{ub}$ è un upper bound di $\Sigma$ se l'insieme dei modelli dell'ipotetico upper bound contiene l'insieme dei modelli della teoria iniziale. Cioè:
$M(\Sigma) \subseteq M(\Sigma_{ub})$ .

Usare upper e lower bound e restringere la ricerca

L'uso di upper e lower bound si ha perchè si rilassa il terzo vincolo dell'elenco sopra esposto, ovvero non si trova proprio un equivalente di SIGMA ma una sua approssimazione per poi risolvere il problema in modo semplice (come abbiamo scritto). Il problema è che se ci accontentiamo che la soluzione vera stia nel range delimitato dall'upper e dal lower bound potremmo avere risultati poco utili, perchè magari il range di possibili teorie tra il LB e L'UB è troppo grande.

Dunque l'obiettivo è restringere la ricerca attorno a $\Sigma$. Si fa osservare che qualora trovassimo un $\Sigma '$ compreso tra il lower e l'upper bound tale per cui è forzata la relazione $M(\Sigma ') = M(\Sigma)$, sostanzialmente abbiamo trovato una teoria equivalente a SIGMA (che è ottimale per la risoluzione del problema se rispetta anche i primi 2 punti dell'elenco stilato prima, ma è una teoria di Horn, poichè è compresa tra lower ed upper bound di Horn, e quindi molto probabilmente li rispetterà).

Greatest lower bound

$\Sigma_{glb}$ teoria di Horn è il greatest lower bound di $\Sigma$ se $\Sigma_{glb}$ è un LB di $\Sigma$ e non esiste nessuna teoria di Horn $\Sigma '$ tale che $M(\Sigma_{glb}) \subseteq M(\Sigma ') \subseteq M(\Sigma)$. Ovvero non esiste nessun SIGMA' con l'insieme dei modelli più vicino a SIGMA rispetto a SIGMA_GLB.

least upper bound

$\Sigma_{lub}$ teoria di Horn è il least lower bound di $\Sigma$ se $\Sigma_{lub}$ è un UB di $\Sigma$ e non esiste nessuna teoria di Horn $\Sigma '$ tale che $M(\Sigma) \subseteq M(\Sigma ') \subseteq M(\Sigma_{lub})$. Ovvero non esiste nessun SIGMA' con l'insieme dei modelli più vicino a SIGMA rispetto a SIGMA_LUB.

Esempio ed uso di GLB e LUB

sigma = { not a or c, 
          not b or c, 
          a or b }
  //sigma è uan teoria proposizionale in forma normale disgiuntiva.

LB  = { a and b and c }
GLB = { a and c }
GLB = { a and b }
LUB = { c }
UB  = { not a or c,
        not b or c }
  //nota: i vari UB e LB sono insiemi di modelli
  //in questo caso sono insiemi formati da un solo modello altrimenti
  //avremmo scritto LUB { {qualcosa}, {qualcosa} }

Nota: come si vede i GLB possono non essere unici, mentre i LUB di solito lo sono.

Ora che conosciamo GLB e LUB che uso ne facciamo?

  1. $\Sigma_{lub} \models \varphi$ . Provo a derivare la formula dal LUB. Se ci si riesce, siccome il LUB ha, in generale, più modelli della teoria di base SIGMA, allora la formula è vera per ogni modello del LUB e quindi per ogni modello della teoria di base. Di conseguenza deduciamo che $\Sigma \models \varphi$ ed abbiamo risolto il problema. Se non ci si riesce, andare al passo 2.
  2. $\Sigma_{glb} \models \varphi$ . Proviamo a derivare la formula con il GLB. Se non ci si riesce vuol dire che almeno un modello del GLB rende falsa la formula, ma poichè i modelli del GLB sono contenuti nei modelli di SIGMA, quel modello che rende falsa la formula è un modello per SIGMA e quindi neanche da SIGMA riusciamo a dedurre la formula. Se ci riusciamo invece non possiamo dire nulla di certo. A questo punto si paga un costo Co-NP e si effettua direttamente $\Sigma \models \varphi$.

Se è possibile, tuttavia, avere che il LUB ed il GLB formano una regione molto stretta (cioè la "distanza" tra GLB e LUB è corta, praticamente è come se avessimo un SIGMA equivalente in forma di teoria di Horn) allora va bene lo stesso perchè si riesce ad estrapolare qualche informazione in più per risolvere il problema in modo semplificato. Se invece la distanza è ampia conviene spender subito le risorse nel calcolo $\Sigma \models \varphi$ , perchè l'ottenimento di ulteriori dati dal range compreso tra LUB e GLB potrebbe esser molto costoso.

Il tempo per calcolare il LUB ed il GLB non è tenuto in conto. Perchè non se ne tiene conto visto che stiamo cercando di pagare un tempo minore di Co-Np ? Perchè si immagina di dover fare query continue al sistema, cioè "SIGMA implica questa formula o no?". Per ogni query spenderemmo Co-NP. Allora conviene spendere molto una sola volta e poi avere un'approssimazione del problema che per ogni query richiede tempo polinomiale piuttosto che spender tempo esponenziale ogni volta.

Teorie consistenti

Teorie soddisfacibili, ovvero dove esiste almeno un modello.

Costo computazionale per il calcolo del GLB

Teorema: qualsiasi teoria SIGMA è consistente se e solo se lo sono il suo GLB ed il suo LUB.

Dubbio (partially solved): almeno un GLB ed un LUB o tutti? Credo che ne basti almeno uno. Perchè se esiste un GLB consistente non può esistere un GLB inconsitente (senza modelli) perchè sarebbe un LB del GLB stesso (per la definizione di inclusione di insiemi di modelli). Analogo per il LUB, anzi un LUB senza modelli implicherebbe un GLB, lol.

Corollario: il calcolo del GLB non può essere polinomiale. Infatti se si potesse trovare il GLB in tempo polinomiale risolveremmo SAT3 in tempo polinomiale, poichè se trovassimo in tempo polinomiale un GLB consistente (assieme ad un LUB analogo per il teorema esposto) allora potremmo rispondere a SAT in tempo polinomiale e ciò non è possibile.

Esponenzialità di SIGMA. Clausole di Horn e clausole di Horn duali.

SIGMA in cosa è esponenziale? Nelle clausole non di Horn o di Horn duali4 che fanno parte della teoria. Ovvero SIGMA è esponenziale nel numero di clausole non di horn presenti in SIGMA stesso. Il fatto è che nella realtà si usano quasi solo teorie di Horn perchè sono più semplici da maneggiare, quindi il problema dell'implicazione (o deduzione) di una formula è in realtà più semplice.

Horn Strengthening. Clausole come insiemi.

Se C è una clausola, $C_H \subseteq C$ è un horn strengthening se rispetta le proprietà:

  1. C_H è una clausola di Horn.
  2. non esiste nessuna clausola C' di Horn tale che $C_H \subset C' \subseteq C$, ovvero non esiste nessuna clausola di horn contenuta in C che contiene C_H.

Esempio:

a or b or not c

C_H
- a or not c
- b or not c
//notare un lett. positivo ed il resto negativi in forma disgiuntiva

non C_H
- not c //poichè ci sono due altre clausole che contengono questa, leggi sopra

Nota: possono esserci più HS per la stessa clausola.
Nota2: se C è una clausola in forma di Horn, per definizioni è l'unico HS ammissibile per se stessa.

In che senso una clausola è contenuta insiemisticamente in un'altra?
Possiamo vedere una clausola come un insieme, e composizioni di clausole come insieme di insiemi.

a or b or not c
diventa
{a, b, not c}

(a or b or not c) and (d or not c)
diventa
{ {a, b, not c}, {d or not c} }

Horn Strengthening di una teoria

Data una teoria SIGMA, un HS di questa è costruito scegliendo un HS di ogni clausola di SIGMA.

Calcolo del GLB tramite Horn-Strengthening

Data una teoria SIGMA e l'insieme delle sue clausole, si generano tutte le possibili teorie SIGMA' pari a tutti i possibili HS di SIGMA. Cioè SIGMA' sono gli HS di SIGMA. Poi si avvia il seguente algoritmo.

In input diamo la teoria SIGMA.
In output riceviamo il GLB.

Si può dare un ordine agli HS della teoria, ad esempio in modo lessicografico.

.Sia L il primo HS, secondo l'ordine, di SIGMA
loop:
  sia L' il successivo HS.
  se L' non esiste -> break.
  se L implica logicamente L' allora L := L' [1]
end loop
  ritorniamoClausoleSussunte(L)
    //può succedere che L sia ridondante, ovvero contiene clausole implicate da altre clausole sempre in L
    //quindi si elimina la ridondanza.

[1] Ovvero L' è più vicino alla teoria (ricordiamoci che stiamo calcolando un GLB), quindi se $L \models L'$ allora $M(L) \subseteq M(L')$, perchè magari L' può esser soddisfata da altri modelli oltre a quelli di L, il contrario, per definizione di deduzione, non è vero.

esempio:

SIGMA = (a or b or not c) or (d or not a)
L'  = { {b, not c}, {d, not a} }
L'' = { {a, not c}, {d, not a} }

L'' viene prima in ordine lessicografico (la 'a' iniziale nell'insieme). L' ed L'' sono due HS di SIGMA

In generale il numero di HS è esponenziale nel numero di clausole non di horn di SIGMA, quindi in generale l'algoritmo per il calcolo del GLB è esponenziale.

La proprietà dell'algoritmo è quella di essere "anytime", ovvero può essere interrotto abbastanza presto e comunque restituirà un risultato parziale.

Quanto un GLB approssima bene la teoria SIGMA ?

Teorema: Ogni teoria logica è equivalente alla disgiunzione dei suoi GLB.


Ovvero calcolando tutti i GLB e poi componendoli in modo disgiuntivo potremmo ottenere una teoria equivalente a SIGMA per il calcolo di $\Sigma_{all GLB} \models \varphi$. Questo calcolo, tuttavia, non sarebbe polinomiale perchè il costo eposnenziale lo pagheremmo nel calcolare tutti i GLB, dunque è la stessa cosa (in generale) di calcolare $\Sigma \models \varphi$ .

Osservazioni su un caso di problema difficile: SAT

SAT è stato uno die primi problemi la cui alta difficoltà è stata dimostrata, quindi vediamo i metodi risolutivi che si sono sviluppati per risolverlo.

Una delle tecniche centrali per risolvere questi problemi è data dall'introduzione di elementi di casualità.

Algoritmo greedy sat

Si ha un algoritmo greedy che viene riavviato in modo casuale.

L'algoritmo greedy si basa sulla seguente idea: dato un assegnamento di verità t per la teoria5 che soddisfa alcune clausole (se soddisfa tutte le clausole l'assegnamento lo si prende come soluzione), consideriamo tutti i vicini di t, cioè $t^{(1)}, \ldots, t^{(n)}$ che differiscono da t per l'assegnamento di verità di una singola variabile. Ovvero ogni assegnamento vicino di t è uguale a t tranne che per una variabile che da vera è diventata falsa. Ovviamente questi vicini sono tanti quanti sono le variabili.

Di questi vicini si sceglie l'assegnamento che soddisfa il maggior numero di clausole e questo numero deve essere maggiore del numero di clausole soddisfatte da t (può anche non esistere un assegnamento simile). Se non si trova un assegnamento che soddisfa un numero maggiore di clausole rispetto a t, allora l'algoritmo è un vicolo cieco e si fa restart.

L'assegnamento iniziale da cui si parte è random.

maxTries, maxFlips sono valori costanti decisi a priori.

for i=1 to maxTries
  begin
    t:= random assignment
    for j:= 1 to maxFlips
      if t satisfy SAT instance 
        return t
      else
        t' := max_val (flip(t))
          //qui si cerca il vicino di t che soddifa più clausole

        /* [1]
        if (val(t') < val(t) ) //se il numero di clausole soddisfatte è minore
          break; //
        */
    end for
  end
end for

Il passo indicato con [1] non ci va e vediamo perchè. Perchè invece di eseguire il restart facciamo comunque un numero fisso di maxFlips, questo ci permetterà a volte di superare gli altipiani o i crinali.
d20.jpg

L'algoritmo in questione riesce a gestire formule (difficili, vedi instanze difficili) di 500 variabili in tempo ragionevole e con le stesse risorse un algoritmo esatto non euristico risolve formule con 140 variabili.

Migliorare Gsat. Gsat wild walking.

Si introduce un ulteriore elemento di randomizzazione quando si sceglie t'.
Con una probabilità fissata 'p' eseguiamo t' := max_val (flip(t)) (di solito p>0.5) .
Con probabilità 1-p si prende una clausola di quelle non soddisfatte (scelta in un certo modo, magari random) e si flippa una variabile di quella clausola. Si osserva che una clausola di sat è i forma disgiuntiva. Quindi se non è soddisfatta vuol dire che nessuna delle variabili nella clausola la soddisfa, basta flipparne una per renderla vera.
Quindi sappiamo solo che t' ora soddisfa quella clausola ma potrebbe non soddisfare tutte le altre.

Con questa modifica, anche poco intuitiva, Gsat WW con le stesse risorse risolve problemi di 2000 variabili invece che solo 500.

Usando simulated annealing con gsat si arriva a risolvere problemi da 800 variabili.

Nota sugli algoritmi euristici

Quando un algoritmo euristico come Gsat o Gsat WW dice "no" non vuol dire che la formula è insoddisfacibile, bensì vuol dire che non ha trovato una soluzione nei tempi richiesti.

Osservazione: le tecniche di randomizzazione ponderate funzionano.

Le tecniche che inseriscono casualità servono per superare crinali e quant'altro, cosa che richiede un costo elevato per gli algoritmi esatti. L'altro dato che si ha è che le tecniche di randomizzazione non sono equivalenti tra loro perchè dipende come si agisce sulla struttura del problema.

Testing degli algoritmi. Usare istanze difficili. Phase transition.

Quando si testano algoritmi risolutivi bisogna usare istanze difficili, e dobbiamo saperlo se l'istanza è difficile o meno.
Per sat un'istanza difficile è: circa la metà degli assegnamenti possibili soddisfano la formula e l'altra metà no.

Per sat si è studiato l'effetto phase transition che è il rapporto tra numero di clausole e vatiabili. Han trovato questa relazione:

d21.jpg

(Phase transition perchè ad un certo punto la curva cambia di pendenza)
Prendiamo un rapporto molto grande, quindi molte clausole e poche variabili. Il problema è facile perchè quasi sicuramente la formula non è soddisfacibile (ad esempio possono capitare due clausole (a) and (not a) ).

Le clausole è come se fossero i vincoli del problema (Ric Op.), le variabili è come se fossero i parametri. Abbiamo pochi parametri per soddisfare i vincoli.

L'altro estremo è poche clausole e molte variabili, in questo caso troveremo più di un assegnamento che soddisfi la formula.

I casi più difficili si hanno quando ci sono un pochino di vincoli in più rispetto ai parametri disponibili.

Il fenomeno della phase transition si è osservato anche in altri problemi e quindi han scoperto che è un fenomeno generale se dimensionato ai giusti vincoli e variabili.

Relazione con quanto detto nella teoria generale.

Abbiamo detto che un problema difficile si risolve o cercando approssimazioni tramite un'euristica o cercando di trasformarlo in problemi noti sui quali si hanno più strumenti d'indagine. SAT è un problema noto ed abbiamo visto alcune euristiche per risolverlo, ma molti problemi vengono tradotti in sat proprio per questo motivo.

Tradurre un problema di [[learning:ai-course:8-planning|planning]] in SAT

Vediamo come tradurre un problema espresso in STRIPS per il mondo dei blocchi in sat.

Modifichiamo alcune cose nella rappresentazione del problema di planning, introducendo degli indici di stato da esplicitare in ogni azione e fluente.

on (a, b, 1)  //fluente
  //'a' e su 'b' nello stato 1
move (a, b, c, 2)
  // muovi a da 'b' su 'c' generando lo stato 2

Questi predicati rappresentano la traduzione in SAT delle azioni strips.

Con questa struttura possiamo rappresentare lo stato iniziale ma qualsiasi stato successivo sarà, in generale, rappresentato parzialmente. Perchè?

  1. Perchè a volte non lo descriviamo completamente (ad esempio c'è il problema del frame, che in strips è un'assunzione).
  2. Perchè non sappiamo prevedere l'indice di alcuni stati, come quello finale. Potremmo inserire una costante molto grande, sotto l'assunzione che se raggiungiamo lo stato finale prima, possiamo fare sempre azioni vuote fino a raggiungere uno stato equivalente a quello finale ma con indice pari alla costante.

Dopo aver definito i predicati si descrivono le clausole (in forma di regole) che descrivono gli effetti delle azioni e le precondizioni di queste.

move (a, b, c, 1) -> clearr (b,2) and on(a,c,2) and not clear (c,2)
  //conseguenze, add e delete list
move (a, b, c, 1) -> clearr (a,1) and on(a,b,1) and clear (c,1)
  //precodizioni (notare l'indice di stato uguale)

Il probelma del frame bisogna affrontarlo esplicitando tutto ciò che resta immutato. Per ogni fluente dovremmo scrivere una roba del genere:

on (d,e,1) and move(a,b,c,1) -> on(d,e,2)
  //cioè se spostiamo qualcosa che non riguarda d ed e, questi rimarranno al loro posto.

Quindi per ogni azione, per ogni fluente e per ogni stato devo scrivere l'insieme di condizioni che riguardano il problema del frame, queste condizioni sono dette "frame axiom".

Poi bisogna esplicitare il fatto che non si possono compiere azioni in conflitto tra loro:

move (a,b,c,1) or not move (a,b,d,1)

Se abbiamo 'a' azioni ed 'f' fluenti la traduzione genera un numero lineare di predicati ground. Il problema è che nell'arità di azioni e fluenti, se consideriamo tutti i possibili casi, il costo è esponenziale ma per ora si tralascia.
Se abbiamo 'a' azioni, 'f' fluenti ed 'n' stati il numero di predicati ground sarà n*(a+f) (tralasciando le combinazioni possibili negli altri parametri di ogni predicato). Vedi sotto i dettagli.

La formula finale al più quanto sarà grande?

  • I frame axioms sono il prodotto azioni*fluenti*stati (per ogni azione, per ogni fluente e per ogni stato) , perchè ogni azione può modificare o meno un fluente in un dato stato.
  • Conseguenze e precondizioni sono dati da azioni*stati*2 , poichè ogni azione in ogni stato genera una clausola di grandezza costante di predicati. Il 2 è dato dal fatto che ci sono clausole per le conseguenze dell'azione e clausole per le precondizioni all'azione.
  • azioni mutualmente esclusive: coppie di azioni che si escludono, quindi un numero quadratico nelle azioni per ogni stato, cioè $a^2\cdot n$ .

Quindi complessivamente ho una dimensione del numero di clausole polinomiale in termini di azioni e fluenti, ma esponenziale se si tiene conto dell'arità di azioni e fluenti. Perchè un conto è considerare on(_, _ , stato) un conto è considerare on(a,b,1), on (a,c,1), etc.. .

Tuttavia possiamo limitare l'esponenzialità. Vediamo un esempio sul predicato move.
move(a,b,c,1) eliminiamo lo stato ed abbiamo arità 3. Con k blocchi avremmo $3^k$ possibili versioni ground del predicato. Se scoppattiamo l'azione in sottopredicati detti descrittori possiamo scrivere:

obj(a) //soggetto dell'azione 
and source(b,1) //sorgente dell'azione con lo stato 
and dest(c,1) //destinazione dell'azione con lo stato

L'intera clausola è l'azione in se. Stessa cosa posso fare con i gluenti.
Quindi l'arità scende perchè per obj ho k elementi, per source k (eliminando lo stato) ed idem per la destinazione.

Dubbio: Si potrebbe dire, ma puoi avere diversi tipi di azioni per lo stesso stato. Cioè io avrei quella clausola di descrittori ripetuta per ogni possibile combinazione e quindi rimane $3^k$.

In questo modo la base rimane uguale ma l'arità scende, anche osservando che posso avere un'azione per stato altrimenti cambio stato.

La traduzione vista è la più semplice anche se esistono traduzioni più efficienti. Simili traduzioni si attuano per molti problemi di ai, passando un problema difficile ad un altro che però è stato studiato di più.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License