5      Applicazioni

Graph Coloring

Hardware

Pianificazione

Scheduling

Se un problema è NP­completo, possiamo in teoria tradurlo nel SAT usando una codifica che è polinomialmente limitata in dimensione. Le ricerche negli ultimi dieci anni hanno mostrato che quest’approccio è spesso notevolmente efficace in pratica.

5.1     Graph Coloring

I problemi di Graph Coloring possono essere codificati facilmente in SAT. Per codificare il problema di kcoloring del grafo con n nodi, utilizziamo  kn variabili, con v_ij vero se il nodo i prende il colore j. È possibile una codifica più compatta che usi nlog₂k variabili in cui v_ij è True se il nodo i ha il colore con il bit j impostato su True. In più, possiamo scegliere di non specificare i vincoli che ogni nodo prende solamente un colore.

Se ad un nodo sono dati due o più colori, possiamo semplicemente scegliere uno a caso. Questo è specialmente utile per i metodi di ricerca locale. Anche Selman e al. hanno riportato che GSAT è competitivo con procedure specializzate di Graph Coloring [116]. Un'eccezione è Hoos, che ha guardato all'effetto delle diverse codifiche di problemi Graph Coloring nel SAT, su algoritmi di ricerca locale come WalkSAT [66]. Un'altra eccezione è la soluzione dei problemi d’esistenza dei quasigroup, che possono essere visti come un tipo specializzato di problemi Graph Coloring.

5.2     Hardware

Problemi come la verifica e la diagnosi dei difetti nell’hardware sono stati obiettivi popolari per la loro codifica nel SAT. Tali problemi sono rappresentati molto spesso nel SAT in modo molto diretto e naturale, specialmente se il modello di circuito ignora i problemi di tempi.

Il segnale in un circuito può essere modellato come variabile booleana che è True se il segnale è alto e False altrimenti. Le porte logiche come NAND sono poi modellate dalla congiunzione logica con lo stesso nome. Per esempio, Larrabee ha generato alcuni problemi SAT basati su una varietà di difetti nei circuiti digitali sincroni incluso single stuck­at e bridge­faults [86]. Come un altro esempio, Kamath, Karmarkar, Ramakrishnan e Resende hanno proposto dei benchmark che codificano i problemi di sintesi di circuiti nel SAT [75 ]. Mentre questi problemi di sintesi di circuiti sono usati in un numero di studi sui metodi di ricerca locale ([112], [114], [116]), loro competono poco con il metodo completo Davis­Putnam.

5.3     Pianificazione

Kautz e Selman hanno avuto successo nel risolvere i problemi di pianificazione, codificandoli nel SAT e utilizzando, sia metodi di ricerca locale come GSAT, che procedure complete come quella di Davis­Putnam con le strategie di randomization e di riavvio [54], [77], [78]. In generale, la pianificazione è un problema più complesso del SAT. Senza restrizioni sugli operatori, la pianificazione è indecidibile. Per codificare i problemi di pianificazione in SAT, si devono fare restrizioni supplementari. La proposta di Kautz e Selman è stata di limitare la lunghezza del piano. Per conservare la completezza questo limite può essere aumentato iterativamente.

Un problema di pianificazione può essere rappresentato come un set di assiomi, per il quale qualsiasi assegnamento soddisfacente corrisponde ad un piano valido. Nel linguaggio di pianificazione ogni predicato è aumentato con un indice di extra time. Per esempio, il predicato move(x,y,z,i) è True se trasportiamo x da y a z all’istante di tempo i.

Kautz e Selman hanno creato a mano le loro codifiche originali con informazioni supplementari di dominio che sono non esprimibili nel linguaggio azione STRIPS. Ernst, Millstein e Weld hanno proposto il sistema di pianificazione MEDIC nel quale la codifica è automatica e si avvicina all'efficienza delle codifiche manuali di Kautz e Selman [24]. Kautz e Selman hanno investigato anche un modo diverso di codificare i problemi di pianificazione nel SAT, basato sulla rappresentazione della pianificazione, utilizzato nel rivoluzionario sistema Graphplan [79].

5.4     Scheduling