Introduzione

Negli ultimi anni, c’è stato un aumento notevole della ricerca AI nella soddisfacibilità proposizionale (SAT). Ci sono molti fattori dietro il crescente interesse in questo settore.

Un primo fattore è il miglioramento delle procedure di ricerca per SAT. Alcune nuove procedure di ricerca locale, come per esempio il GSAT, sono capaci di risolvere problemi SAT con migliaia di variabili. Nello stesso tempo, le implementazioni degli algoritmi di ricerca completa, come quello di DavisPutnam, sono stati capaci di risolvere molti problemi matematici. Un altro fattore è l'identificazione dei problemi SAT difficili con la transizione di fase nella solubilità.

Un terzo fattore è la dimostrazione che possiamo spesso risolvere problemi del mondo reale codificandoli nel SAT. Inoltre, c’è stato anche un miglioramento della comprensione teoretica del SAT.

1.1 Problemi AI, logica, e ricerca

Il ruolo generale dell’AI è di realizzare un comportamento intelligente nelle macchine, idea che è stata anche alla base della costruzione dei primi computer. Da quando questa motivazione di base è strettamente correlata con questioni generali riguardanti l'intelligenza, l’apprendimento ed il lavoro della mente umana, i problemi dell’AI sono spesso, se non sempre, riferiti a discipline totalmente diverse da quelle riguardanti i computer, come psicologia, filosofia e neurobiologia. Alcuni dei problemi più rilevanti nell’AI sono le aree del riconoscimento vocale, la dimostrazione di problemi, i giochi, e la composizione musicale. Sfortunatamente, la maggior parte di questi compiti comportano problemi computazionali molto difficili e nonostante i successi impressionanti in molte aree dell’AI, mancano soluzioni soddisfacenti e fattibili a molti problemi dell’AI.

Come tutti i problemi della scienza dei computer, i problemi AI possono essere suddivisi in due grandi categorie: problemi di rappresentazione e problemi computazionali. Il primo tipo di problema comporta trovare una rappresentazione appropriata o formalizzazione di un problema da qualche dominio, mentre il secondo tipo consiste nel trovare gli algoritmi per risolvere questi problemi. Chiaramente, gli entrambi tipi di problemi si intrecciano, quanto tempo la risoluzione di un problema dal mondo reale richiede di trovare una rappresentazione appropriata e concepire un algoritmo che risolva il problema formalizzato. Inoltre, la costruzione e l’implementazione degli algoritmi risolutori di problemi dipendono spesso in modo critico dalla rappresentazione appropriata del problema.

Nell’AI, i problemi sono spesso rappresentati attraverso le logiche formali. Una logica formale L è data da un linguaggio formale che specifica la sintassi delle espressioni logiche, ed il mapping di queste espressioni in un sistema di costanti logiche che specificano la semantica di L. Esempi di logiche formali che sono spesso utilizzate e studiate nell’AI sono la logica proposizionale, la logica di primo ordine, del secondo ordine, la logica modale, la logica temporale.

In un sistema logico dato, le proposizioni che sono True sono chiamate teoremi.

I teoremi possono essere dimostrati semanticamente, utilizzando il ragionamento formale fuori del sistema logico.

Alternativamente, il meccanismo sintattico di dimostrazione chiamato calculi può essere utilizzato per stabilire la verità o la falsità delle proposizioni logiche.

Un calcolo logico è un sistema formale che consiste in un set di assiomi che sono proposizioni elementari vere, ed un set di regole che definiscono le trasformazioni che conservano la verità delle frasi. Calculi è la base per l'automatizzazione della logica. Per qualche sistema logico, ci sono proposizioni semanticamente vere che non possono essere dimostrate algoritmicamente. In queste logiche, il teorema è non risolvibile. La logica del primo ordine è di questo tipo, mentre per la logica proposizionale la validità delle proposizioni può essere decisa algoritmicamente.

Molti problemi dell’AI, particolarmente quelli che sorgono nel contesto delle logiche formali, sono problemi di decisione, dove le soluzioni sono caratterizzate da un set di condizioni che devono essere soddisfatte per risolvere il problema. Il risolutore di problemi classico è formulato al solito come un problema di decisione. Comunque, i problemi dai domini applicativi sono spesso piuttosto problemi di ottimizzazione che di decisione. I problemi di ottimizzazione possono essere considerati generalizzazioni dei problemi di decisione, dove le soluzioni sono valutate da una funzione obiettivo. Ci sono due tipi dei problemi di ottimizzazione, una versione di massimizzazione ed una di minimizzazione. Per questi problemi, lo scopo è di trovare soluzioni ottimali, per esempio soluzioni con valore massimo, rispettivamente minimo, della funzione obiettivo.

In molti casi nell’AI, i problemi di decisione e di ottimizzazione possono essere caratterizzati come problemi di ricerca, per esempio problemi che richiedono una ricerca attraverso un numero di soluzioni candidato o soluzioni parziali, mentre si tenta di trovare una soluzione valida, e forse ottimale, per le istanze del problema dato. Molti problemi di gioco, dimostrazioni di teoremi, possono essere formulate come problemi di ricerca. Notiamo che gli algoritmi per risolvere i problemi di ricerca non necessitano essere sempre degli algoritmi classici di ricerca.

Come menzionato prima, molti problemi dell’AI sono molto difficili computazionalmente. Usando la metafora della ricerca, di solito questo è riflesso dal fatto che per le istanze di un problema dato, il set delle soluzioni candidato o delle soluzioni parziali, che definiscono lo spazio in cui ha luogo la ricerca, è molto grande e non sono conosciuti metodi algoritmici per trovare soluzioni efficaci in questi enormi spazi di ricerca.

Una situazione tipica è il caso dei problemi dove la complessità temporale per trovare soluzioni cresce esponenzialmente con la dimensione del problema, mentre la decisione se una soluzione candidato è reale può essere fatta in tempo polinomiale.

1.2 Ricerca sistematica confrontata con la ricerca locale

Gli algoritmi di ricerca sistematica esaminano lo spazio di ricerca delle istanze di un problema in maniera sistematica, garantiscono di trovare una soluzione, oppure se nessuna soluzione esiste, questo fatto è determinato con certezza. Questa proprietà tipica degli algoritmi, basata sulla ricerca sistematica si chiama completezza.

D'altra parte la ricerca locale inizia la ricerca in qualche punto dello spazio di ricerca, e poi procede con movimenti iterativi, dalla posizione presente verso una posizione vicina (contigua), dove la decisione ad ogni passo è basata solamente sulla conoscenza locale. Anche se le decisioni locali sono fatte in un modo sistematico, gli algoritmi di ricerca tipicamente locali sono incompleti. Anche se le istanze del problema dato hanno una soluzione, loro non garantiscono di trovarla. I metodi di ricerca locale possono visitare la stessa posizione all'interno dello spazio di ricerca più di una volta. Esiste anche la possibilità di bloccarsi frequentemente da qualche parte nello spazio di ricerca, e questa posizione non possono abbandonarla senza meccanismi speciali, come un nuovo riavvio del processo di ricerca od un altro genere tipo di meccanismo.

Sembrerebbe che, dovuto alla loro incompletezza, gli algoritmi di ricerca locale sono generalmente inferiori a quelli sistematici. Ma, come vedremo più avanti, questo non è vero. Molti problemi sono impliciti di natura, si sa che sono risolvibili e quello che si richiede è di ottenere una soluzione, invece di decidere solamente l’esistenza di una soluzione. Questo è valido in particolare per i problemi di ottimizzazione, come il Problema del Commesso Viaggiatore (TSP) che consiste nel trovare una soluzione di sufficiente ottimalità, ma anche per problemi di decisione con sottovincoli che sono abbastanza comuni.

Secondo, in un tipico scenario applicativo, il tempo per trovare una soluzione è spesso limitato. Esempi per tali problemi di realtime, possono essere trovati in tutti i campi applicativi. Quasi ogni problema del mondo reale che comporta un’interazione con il mondo reale, ha vincoli di realtime. In queste situazioni, gli algoritmi sistematici devono essere spesso interrotti dopo che il tempo allocato è stato esaurito, e questo chiaramente li rende incompleti. Questo è particolarmente problematico per gli algoritmi sistematici di ottimizzazione che cercano attraverso gli spazi delle soluzioni parziali; se quelli di solito sono interrotti non è disponibile nessuna soluzione candidato, mentre nella stessa situazione, gli algoritmi di ricerca locale offrono tipicamente la migliore soluzione trovata finora [1]. Idealmente, gli algoritmi per problemi di realtime devono essere capaci di consegnare soluzioni ragionevolmente buone, in qualsiasi punto, durante la loro esecuzione. Per i problemi di ottimizzazione, questo significa che il run-time e la qualità della soluzione devono essere correlati positivamente, per i problemi di decisione si potrebbe immaginare di indovinare una soluzione quando accade un timeout, dove l'accuratezza dell’ipotesi dovrebbe aumentare con il run-time dell’algoritmo. Questa così detta proprietà di anytime dell’algoritmo, è di solito difficile da realizzare, ma in molte situazioni il modello di ricerca locale sembra andar meglio per concepire algoritmi anytime che modelli di ricerca sistematica.

Come una questione di fatto, gli algoritmi di ricerca sistematica e locale sono leggermente complementari nelle loro applicazioni. Un bell’esempio può essere trovato in [78 ], dove un algoritmo veloce di ricerca locale è utilizzato per trovare soluzioni per problemi di pianificazione, l’ottimalità di cui è dimostrata per mezzo di algoritmi sistematici. Diverse prospettive dello stesso problema possono in certi casi appellare ad algoritmi di ricerca locale, se sono richieste soluzioni buone in un tempo corto usando un calcolo parallelo e la conoscenza riguardo il dominio del problema è molto limitato. In altri casi, se sono richieste delle soluzioni esatte od ottimali, il vincolo del tempo è meno importante e possono essere sfruttate alcune conoscenze sul dominio di problema; in questo caso la ricerca sistematica sarà la scelta migliore. Finalmente, è evidente che per alcune classi di problemi, i metodi di ricerca locale e sistematica sono efficaci soprattutto per diverse sottoclassi di istanze.

Sfortunatamente, la questione generale su quando preferire il metodo di ricerca sistematica e quando quello locale rimane aperta.

Gli algoritmi di ricerca locale spesso si avvalgono pesantemente di meccanismi stocastici, come le euristiche. Questi algoritmi sono chiamati algoritmi di ricerca locale stocastica (SLS), e sono usati da molti anni nel contesto di problemi di ottimizzazione.

Fra gli algoritmi più rilevanti troviamo l'algoritmo di LinKernighan per il problema del commesso viaggiatore, così come metodi generali come la ricerca tabu [50], e simulated annealing [82]. Ultimamente è diventato evidente che gli algoritmi stocastici di ricerca locale, possono essere applicati con successo nella risoluzione di problemi di decisione NPcompleti, come il Graph Coloring Problem GCP [59], [96], [97] od il problema di soddisfacibilità nella logica proposizionale SAT [116], [35], [56].

Il secondo è particolarmente interessante per la ricerca nell’AI, in quanto non è soltanto uno dei problemi di base che sorgono nel contesto dell’approccio basato sulla logica, ma si può utilizzare anche nel contesto dell’approccio del risolutore generico di problemi dove problemi di base da altri domini, come Blocksworld Planning o Graph Coloring, sono risolti codificandoli nel SAT. In seguito si risolvono le istanze codificate usando tecniche stocastiche di ricerca locale. I recenti risultati della ricerca indicano che quest’approccio è vitale per almeno alcuni domini di problemi [78], [68] e di conseguenza oggi c'è un considerevole interesse, non solo nella comunità dell’AI, ma anche nelle questioni connesse a lui.

1.3 Risolutore di problemi con ricerca locale stocastica

L'interesse in algoritmi efficienti per problemi astratti e semplici, come il problema della soddisfacibilità nella logica proposizionale SAT, è basato sulla nozione di risolutore generale di problemi. Ci sono due versioni di quest’approccio indiretto, la più debole si basa sulla premessa che possono essere identificate delle tecniche generali per trattare con una serie larga di classi di problemi.

La versione più forte, partendo dal presupposto che è possibile risolvere problemi trasformandoli in qualche dominio, per il quale è disponibile un risolutore universale. Le soluzioni che sono così ottenute sono poi trasformate indietro, nel dominio del problema originale, che fornisce le soluzioni desiderate per il problema.

Quest’approccio di risolutore generico di problemi conta su un numero di premesse:

· prima di tutto, il dominio in cui i problemi sono trasformati (il dominio intermedio) deve fornire sufficiente potere espressivo, in modo tale che un numero significativo di classi di problemi deve essere rappresentabile in questo dominio;

· in seguito, la complessità delle trasformazioni tra i domini dovrà essere sufficientemente bassa confrontata alla complessità per trovare una soluzione, altrimenti le spese generali di questo approccio indiretto potrebbe superare facilmente i suoi vantaggi.

· finalmente, la premessa più importante è l'esistenza di un risolutore sufficientemente generale nel dominio intermedio.

Si potrebbe argomentare che queste premesse sono critiche, nel senso che almeno per alcune di loro, c'è il dubbio su come possono essere incontrate in pratica. C'è un numero di domini che sono espressivi sufficientemente per rappresentare una larga varietà di classi di problemi. Per alcuni di questi, come il SAT ed il CSP, sono state trovate trasformazioni efficienti per molte classi di problemi, in modo tale che abbiamo indicazioni riguardo i costi addizionali della codifica / decodifica, che sono quasi trascurabili quando comparati ai costi per trovare le soluzioni.

Molto probabilmente ci sarà un collegamento stretto tra il problema da codificare e le prestazioni dell’algoritmo dato. Presumendo che si potrebbe trovare un algoritmo di dominio intermedio che raggiunge prestazioni ragionevoli su qualche codifica, per un’ampia serie di problemi, ancora non è chiaro se trovare codifiche appropriate è meno difficile che concepire algoritmi specializzati per i domini applicativi originali. Di conseguenza, il problema cruciale dell’approccio del risolutore generico di problemi è di trovare un algoritmo di dominio intermedio ed un numero di strategie di codifica abbastanza efficaci e semplici, che mostrino performance ragionevoli su un’ampia serie di problemi.

D'altra parte i vantaggi dell'approccio di risolutore generico sono ovvi. Prima di tutto, non c’è bisogno di nessun risolutore specializzato per il dominio del problema originale. Anche altri domini beneficiano dai miglioramenti dei risolutori di domini intermedi.

La versione debole dell’approccio di risolutore generico di problemi è ampiamente accettata nell’AI ed in molte tecniche per risolvere problemi, quali si sa di poter essere applicate con successo ad una varietà di domini di problemi. La variante forte, invece, è meno accettata. Ciononostante, i recenti risultati nel risolvere problemi codificati SAT, utilizzando tecniche di ricerca locale stocastica, danno alcune indicazioni sull'applicazione pratica della versione forte del risolutore.

Ci sono molte ragioni in relazione al SAT come un promettente dominio intermedio:

· Prima di tutto, SAT è NPcompleto, significa che ogni problema NP-completo può essere ridotto polinomialmente al SAT. Così, esistono trasformazioni efficaci tra i problemi SAT e altri problemi di decisione NP-completo. Dato che la classe di problemi di decisione NPcompleto copre una serie larga di problemi applicativi, SAT è abbastanza espressivo da agire come un dominio intermedio.

· Il secondo vantaggio del SAT è la sua semplicità concettuale. In quanto la sintassi, così come la semantica del SAT è molto semplice, specialmente quando limitato alle formule CNF, il SAT offre vantaggi sostanziali per ideare e valutare algoritmi.

Quindi, se il SAT sembra essere una scelta ragionevole per il dominio intermedio, perché non considerare gli algoritmi SLS come risolutori SAT?

Prima, come già menzionato, gli algoritmi SLS possono essere competitivi oppure anche superiori a quelli sistematici sia per i problemi SAT nativi, che per una larga serie di problemi da altri domini codificati nel SAT. Inoltre, la maggior parte degli algoritmi popolari SLS per il SAT sono relativamente facili da implementare perché sono concettualmente abbastanza semplici. Finalmente, la maggior parte di questi algoritmi SLS offre la facilità del confronto.

· Prima, gli algoritmi SLS tipici sono incompleti - non garantiscono di trovare una soluzione se esiste.

· Questi algoritmi sono estremamente non deterministici, che qualche volta è considerato un problema isolato (per esempio, quando sia affronta l'affidabilità e la riproducibilità dei risultati).

· Un inconveniente più importante è il fatto che questi algoritmi sono stati trovati estremamente difficili da analizzare e di conseguenza c'è poca comprensione teoretica del loro comportamento.

Ciononostante, i vantaggi, specialmente le performance superiori che possono essere raggiunte per tipi diversi di problemi SAT, sembrano superare tutti questi inconvenienti in modo tale che gli algoritmi SLS sono considerati ad essere fra i metodi più promettenti per risolvere problemi grandi e difficili di soddisfacibilità.

1.4 Problemi NPcompleti e NPhard

Oggi, la teoria della complessità computazionale è un campo con considerevole impatto su altre aree della scienza del computer. Nel contesto di questo lavoro, il campo primario di applicazione degli algoritmi di ricerca locale stocastica è rappresentato da una classe di problemi computazionalmente molto difficili, per la quale non si conoscono degli algoritmi efficienti. Inoltre, una grande maggioranza di esperti nella teoria della complessità pensa che sia impossibile l'esistenza di algoritmi efficienti per questi problemi.

La complessità di un algoritmo è definita in base al modello di macchina formale. Di solito, questi sono idealizzati, creati in un modo che facilitino il ragionamento formale riguardante il loro comportamento. Uno dei primi, e ancora forse il più evidente di questi modelli, è la macchina Turing. Per le macchine Turing e altre macchine formali, la complessità computazionale è definita in termini di requisiti di spazio e tempo per la computazione.

Di solito la teoria della complessità tratta con intere classi di problemi (generalmente set numerabile di istanze di problemi) invece di singole istanze. Per un algoritmo dato o modello di macchina, la complessità della computazione è caratterizzata dalla dipendenza funzionale fra la dimensione di una istanza e il tempo e lo spazio richiesti per risolvere quest’istanza. Per ragioni di trattabilità analitica, molti problemi sono formulati come problemi di decisione, e le complessità temporale e spaziale sono analizzate in termini del peggiore comportamento asintotico.

Data una definizione appropriata della complessità computazionale di un algoritmo per uno specifico problema, la complessità della classe di problemi può essere definita come la complessità del migliore algoritmo su questa classe di problemi. In quanto la complessità temporale rappresenta generalmente il fattore più restrittivo, le classi di problemi sono suddivise in classi di complessità riguardando il loro caso peggiore di complessità temporale.

· la classe di problemi P, che possono essere risolte da una macchina deterministica in tempo polinomiale;

· la classe di problemi NP, che possono essere risolte da una macchina non deterministica in tempo polinomiale.

Chiaramente, ogni problema in P è anche inclusa in NP, fondamentalmente perché i calcoli deterministici possono essere emulati su macchina non deterministiche. Comunque, la domanda se anche NP Í P, e di conseguenza P = NP, è uno dei problemi più rilevanti della scienza dei computer. Da quando molti dei problemi fondamentali sono in NP, ma possibilmente non in P (non è conosciuto nessun algoritmo deterministico in tempo polinomiale), questo così chiamato P=NP-problem non è soltanto di interesse teoretico. Per questi problemi computazionalmente difficili, il miglior algoritmo conosciuto finora ha complessità temporale di tipo esponenziale. Perciò, con il crescere della dimensione dei problemi, le istanze dei problemi diventati rapidamente intrattabili, hanno poca efficacia sulla dimensione delle istanze del problema risolvibile in tempo ragionevole. Esempi ben conosciuti di problemi NPhard includono il problema della soddisfacibilità SAT, il problema Graph Coloring GCP, il problema del Commesso Viaggiatore TSP ed i problemi di scheduling.

Molti di questi difficili problemi NP possono essere tradotti in ogni altro in tempo polinomiale deterministico. Un problema che è alquanto difficile come alcun altro problema in NP (nel senso che ogni problema in NP può essere ridotto polinomialmente a lui) è chiamato NPhard. Così, i problemi NPhard in un certo senso possono essere considerati altrettanto difficili come ogni problema in NP.

I problemi NPhard che sono contenuti in NP sono chiamati NPcompleti; in un certo senso questi problemi sono i più difficili in NP.

Un risultato fondamentale della teoria della complessità indica che, per dimostrare che NP=P, è sufficiente trovare un algoritmo deterministico in tempo polinomiale per un singolo problema NPcompleto. Questa è la conseguenza del fatto che tutti i problemi NP-completi possono essere codificati reciprocamente in tempo polinomiale. Oggi, la maggior parte degli scienziati pensa che P ¹ NP; comunque, da lontano tutti gli sforzi per trovare una prova per quest’ineguaglianza sono stati senza successo, e ci sono alcune indicazioni che i metodi matematici odierni siano troppo deboli per risolvere questo problema fondamentale.

Molti problemi dai domini applicativi, come i problemi di scheduling e di pianificazione, sono in sostanza NP-completi, ed in generale non risolvibili efficientemente. Comunque, un problema essendo NPcompleto o NP-hard, non vuol dire che è impossibile risolverlo efficientemente. Ci sono almeno in pratica, tre modi di trattare con questi problemi:

· tentare di trovare una sottoclasse relativa del problema che può essere risolta efficientemente;

Dobbiamo ricordare riguardo alla prima strategia, che NPhardness è una proprietà di una intera classe di problemi P, mentre in pratica accade spesso solamente per le istanze di una certa sottoclasse P’Í P. Chiaramente, in generale P’ non potrà essere NPhard, mentre per P potrebbe non esistere un algoritmo efficiente, ma è probabile che sia ancora possibile trovare un algoritmo efficiente per la sottoclasse P’.

Comunque, se il problema è di ottimizzazione e non può essere ristretto ad una sottoclasse efficientemente risolvibile, un'altra scelta potrebbe essere di accettare le approssimazioni di una soluzione invece di tentare di calcolare le soluzioni ottimali. Così, in molti casi la complessità computazionale del problema potrebbe essere ridotta sufficientemente per far diventare risolvibile il problema. In alcuni casi, consentendo un piccolo margine rispetto alla soluzione ottimale, si può risolvere deterministicamente il problema in tempo polinomiale. In altri casi, il problema di approssimazione rimane NPhard, ma la riduzione dello sforzo computazionale è sufficiente per trovare soluzioni delle istanze del problema accettabili.

Comunque qualche volta non possono essere concepiti schemi di approssimazione efficienti, oppure il problema è un problema di decisione al quale non può essere applicato per niente la nozione di approssimazione. In questi casi, un’altra scelta è di concentrarsi su algoritmi probabilistici piuttosto che su quelli deterministici. Ad un primo sguardo, quest’idea ha una certa importanza: secondo la definizione della classe di complessità NP, almeno i problemi NP-completi possono essere risolti efficientemente da macchine non deterministiche. Certo, questo è di poco uso pratico, dato che per un algoritmo probabilistico questo vuol dire che, c'è in ogni caso un'opportunità piccola, di poter risolvere il problema dato in tempo polinomiale. In pratica, la probabilità di successo di tale algoritmo può essere arbitrariamente piccola. Tuttavia, in numerose occasioni, sono stati trovati algoritmi probabilistici che sono stati più efficienti sui problemi NPcompleto o NPhard dei migliori metodi deterministici disponibili. In altri casi, i metodi probabilistici e deterministici si completano reciprocamente nel senso che, per certi tipi di istanze di problemi, sono stati trovati ad essere superiori sia l’uno che l'altro. Fra i problemi più importanti e conosciuti da questa categoria, sono i problemi della soddisfacibilità nella logica proposizionale SAT e con soddisfacimento di vincoli CSP.

1.5 Logica proposizionale e soddisfacibilità

1.5.1 Logica proposizionale

La logica proposizionale è basata su un linguaggio formale basato su un alfabeto che comprende i simboli proposizionali, le costanti logiche e gli operatori logici. Usando gli operatori logici, i simboli proposizionali e le costanti logiche sono combinati in formule proposizionali che rappresentano le espressioni proposizionali. Formalmente, la sintassi della logica proposizionale può essere definita dalla:

Definizione 1.1 (la sintassi della logica proposizionale)

Gli assegnamenti sono mappature dei simboli proposizionali nella tavola di verità. Usando le interpretazioni standard dei connettivi logici sulle costanti logiche, le assegnazioni possono essere usate per valutare le formule proposizionali. Così, noi possiamo definire la semantica della logica proposizionale:

Definizione 1.2 (la semantica della logica proposizionale)

Figura 1 .2: Le tavole di verità dei connettivi logici implicazione e equivalenza

Dovuto al fatto che il set di simboli di una formula proposizionale è sempre limitato, anche il set completo delle assegnazioni per una formula data è limitato. Più precisamente, per una formula che contiene n simboli ci sono esattamente 2ⁿ assegnamenti di simboli.

1.5.2 Soddisfacibilità

“Lei è capo del protocollo per il ballo all’ambasciata. Il principe vi consiglia di invitare Perù o di escludere Qatar. La regina vi chiede di invitare o Qatar o Romania o entrambi. Il re, in un umore dispettoso, vuole offendere sia Romania che Perù, oppure entrambi. Esiste un elenco degli ospiti che soddisferà i capricci dell’intera famiglia reale?”.

Vedremo in seguito come questo problema può essere rappresentato come un problema di soddisfacibilità proposizionale. Definiamo la soddisfacibilità come segue:

Definizione 1.3 (Soddisfacibilità & Validità)

Definizione 1.4 (i problemi SAT e VAL)

1.5.3 Forme normali

Spesso, i problemi come SAT e VAL sono studiati per classi sintatticamente ristrette di formule. Imponendo delle restrizioni sintattiche di solito sono facilitati gli studi teoretici e possono essere anche molto utili per semplificare la progettazione dell’algoritmo. Le forme normali sono formule sintatticamente ristrette in modo tale che per una formula arbitraria F c'è sempre almeno una formula in forma normale F’. Così, ogni forma normale induce una sottoclasse di formule proposizionali che è altrettanto potente come la logica proposizionale. Poiché per certe classi di formule sintatticamente ristrette non è provato se loro sono o non sono forme normali, useremo il termine forma normale in un senso più generale, coprendo sottoclassi della logica proposizionale che è caratterizzata da restrizioni sintattiche. Alcune delle forme normali comunemente utilizzate sono classificate dalle seguenti definizioni.

Definizione 1.5 (forme normali)

Possiamo anche, mettere dei vincoli sulla dimensione delle clausole nel problema. Per esempio, kSAT è la classe di problemi di decisione nella quale tutte le clausole sono di lunghezza k. kSAT è NPcompleto per qualsiasi k£3 ma è polinomiale per k=2 [ 31 ]. Il problema di ottimizzazione MaxSAT è collegato strettamente al problema di decisione SAT.

Dato un set di clausole, qual’è il numero massimo di clausole che possono essere soddisfatte?

Con alcune semplici modifiche, molte delle procedure complete e di approssimazione per SAT possono essere adattate per risolvere i problemi di MaxSAT.

Ritornando all’esempio considerato precedentemente [1.5.2], possiamo esprimere i tre vincoli tramite una formula proposizionale:

dove P, Q e R sono variabili booleani che sono True se e solamente se noi invitiamo, rispettivamente, Perù, Qatar e Romania. Una soluzione al problema è un assegnamento soddisfacente, un assegnamento dei valori di verità alle variabili booleane che soddisfano la formula proposizionale. In questo caso, ci sono solo due assegnazioni soddisfacenti (delle otto possibili). Queste assegnano a P e Q il valore True e ad R il valore False, oppure assegniamo False a P e Q e True a R.

Ovvero, o possiamo invitare gli entrambi Perù e Qatar e offendere Romania, o possiamo invitare solo la Romania e offendere sia Perù che Qatar. La soddisfacibilità proposizionale è un problema molto semplice e rappresenta un elemento importante nella teoria della complessità computazionale. È stato mostrato che la soddisfacibilità proposizionale è stato il primo problema ad essere NPcompleto [13 ]. Nonostante un quarto di secolo di sforzi, esso resta una questione aperta anche se nel caso peggiore, problemi di questo tipo possono essere risolti in tempo polinomiale. Come i migliori algoritmi completi sono esponenziali, generalmente NPcompletezza si considera marcare il confine tra la trattabilità e l'intrattabilità. Ciononostante, la ricerca negli ultimi anni ha mostrato che spesso i problemi di soddisfacibilità possono essere efficientemente risolti in pratica.

1.6 Problemi con soddisfacimento di vincoli (CSP)

Un problema con soddisfacimento di vincoli (CSP) è definito da un set di variabili, ognuna delle quali può prendere un numero di valori da qualche dominio ed un insieme di vincoli che riguardano una o più variabili. Possono essere definiti vari tipi di CSP in base al fatto che i domini delle variabili sono di tipo discreto o continuo, finiti o infiniti.

Definizione 1.6 (CSP discreto e limitato)

Certamente, per questo tipo di CSP il set di tutti gli assegnamenti possibili è limitato. In modo simile al SAT, la classe CSP discreto e finito è NPcompleto. Questo può essere provato facilmente cosi come c’è un stretto collegamento tra il SAT ed il CSP discreto e finito: il SAT sulle formule CNF corrisponde direttamente ad un CSP discreto finito dove tutti i domini contengono solamente i valori booleani T e F, ed ogni vincolo contiene esattamente tutti gli assegnamenti soddisfacenti di una particolare clausola. Viceversa, ogni CSP discreto finito può essere trasformato direttamente in una istanza SAT, dove ogni variabile proposizionale rappresenta un particolare assegnamento di una variabile CSP e ogni vincolo è rappresentata da un numero di clausole. Notiamo che generalmente questo tipo di codifica diretta non produce una formula CNF, ma una formula in CDNF, quale può essere poi trasformata in CNF.

Anche se CSP sembra essere più adeguato del SAT per la rappresentazione di problemi combinatoriali difficili, il SAT è un dominio sintatticamente più semplice, e perciò progettare ed analizzare algoritmi tende ad essere più facile per il SAT che per il CSP. Nello stesso tempo, possono essere generalizzati direttamente in CSP più algoritmi SLS per il SAT.

Di conseguenza, i concetti e gli algoritmi per i risolutori SAT sono più avanzati in molti particolari dello sviluppo corrispondente in CSP.

1.7 Problemi random

Nel modello con clausole di lunghezza fissa (spesso chiamato il modello kSAT random), generiamo problemi con N variabili e L clausole come segue: per ogni clausola è selezionato un sottoinsieme random di dimensione k delle N variabili, e ogni variabile è fatta positiva o negativa con probabilità 1/2. Così, tutte le clausole hanno la stessa dimensione.

Nel modello a probabilità costante, generiamo ognuna delle L clausole del problema, includendo con probabilità p ognuno dei 2N letterali possibili. Dopo l’inclusione delle clausole vuote od unità i problemi diventano più facili, cosi, molti studi utilizzano una versione del modello a probabilità costante proposto in [62] in cui, se una clausola generata contiene solamente uno o nessun letterale, è scartata ed è generata un'altra clausola al suo posto. Noi chiamiamo questo il modello CP.

[1] Si deve notare che, gli algoritmi di ricerca locale possono essere anche progettati in modo tale che possono cercare in uno spazio delle soluzioni parziali

Indietro	Home	Avanti
Abstract	SAT Solver	Procedure complete