Soddisfacibilità booleana

Da Wikipedia, l'enciclopedia libera.

Questa voce riguardante un argomento di matematica non è ancora stata tradotta completamente dalla lingua inglese. Se sei in grado, potresti contribuire a terminarla. Il testo da tradurre potrebbe essere nascosto: clicca su modifica per visualizzarlo. Non usare programmi di traduzione automatica.

Quello della Soddisfacibilità è il problema di determinare se le variabili di una data formula booleana possano essere assegnate in modo che la formula sia valutata "TRUE". Ugualmente importante è individuare che tale assegnamento non esiste, arrivando a concludere che la funzione espressa dalla formula è identicamente "FALSE" per tutti i possibili assegnamenti delle sue variabili. In quest'ultimo caso si dice che la funzione è insoddisfacibile; altrimenti, soddisfacibile. Per enfatizzare la natura binaria di tale problema, ad esso ci si riferisce spesso come al problema di soddisfacibilità booleana o soddisfacibilità proposizionale. Il diminuitivo "SAT" è una sigla comunemente utilizzata per denotare tale problema, dove si intende implicitamente che la funzione e le sue variabili sono tutte valutate in modo binario.

[modifica] Definizioni di base, terminologia e applicazioni

La definizione formale di SAT richiede che la funzione sia epressa nella forma normale clausale (CNF), ovvero come un AND di clausole ognuna formata da un OR di letterali. In tale forma una clausola agisce come un vincolo sui possibili valori che le variabili che la compongono possono avere. Ad esempio la clausola (A OR ~B OR C) è soddisfatta da tutti gli assegnamenti FALSE-TRUE possibili tranne che A = C = FALSE e B = TRUE. Una formula in CNF può, inoltre, essere vista come un sistema di vincoli nello spazio degli assegnamenti binari delle sue variabili. Per estendere questo concetto è utile notare l'esistenza di un altro tipo di "sistema di vincoli", come i sistemi di disequazioni lineari su variabili reali o intere che individuano una regione ammissibile (e quindi degli assegnamenti ammissibili) in programmazione lineare e programmazione lineare intera. La regione ammissibile di una formula CNF contiene precisamente quei valori che rendono la formula valutabile come TRUE.

Nella teoria della complessità il problema Soddisfacibilità Booleana (SAT) è un problema decisionale, la cui istanza è una espressione booleana formata da operatori AND, OR, NOT, "(", ")" applicati a variabili e insiemi di variabili.

La domanda è la seguente: data una espressione, esiste un qualche assegnamento di valori TRUE e FALSE tali da rendere l'intera espressione vera? Una formula di logica proposizionale è detta soddisfacibile se esiste tale assegnamento. La classe di formule proposizionali soddisfacibili è NP-completa. Il problema SAT è di importanza centrale in molte aree dell'informatica, incluse l'informatica teorica, lo studio degli algoritmi, la progettazione dell'hardware, ecc.

Il problema può essere significativamente ristretto benché rimanga NP-completo. Applicando infatti i Teoremi di De Morgan possiamo assumere che gli operatori NOT siano solo applicati alle variabili, e mai a espressioni; ci riferiamo ad una variabile o alla sua negazione come ad un letterale. Ad esempio, sia x₁ e not(x₂) sono letterali, il primo positivo e il secondo negativo. Se facciamo l'OR di un gruppo di letterali, creiamo come detto una clausola, come (x₁ or not(x₂)). Per ultimo consideriamo le formule che sono congiunzione (AND) di clausole - appunto operiamo in CNF. Determinare se la formula sia soddisfacibile o meno è ancora NP-completo, anche se le clausole sono tutte limitate ad avere al massimo tre letterali. Questo particolare problema è detto 3SAT, 3CNFSAT, o 3-soddisfacibilità.

D'altra parte, se restringiamo ogni clausola ad avere massimo due letterali, allora il problema risultante, detto 2SAT, è NL-completo. In alternativa, se ogni clausola fosse una clausola di Horn, contenente al massimo un solo letterale positivo, il problema risultante Horn-soddisfacibilità sarebbe P-completo.

Il Teorema di Cook prova che SAT è NP-completo, ed anzi fu questo il primo problema decisionale ad essere dimostrato appartenente alla classe NP-completo. Al di là del significato teorico di tale dicitura, nell'ultimo decennio si sono avuti enormi passi avanti nella nostra abilità, tramite algoritmi efficienti e scalabili, di risolvere SAT con decine di migliaia di variabili e milioni di vincoli. Esempi di questi problemi sono presenti in model checking, EDA, FPGA, sintesi logica, ecc..

[modifica] Complessità

[modifica] NP-completezza

Prima del 1971 e del Teorema di Cook il concetto di problema NP-completo non esisteva affatto. Tale problema, si è visto, resta di questa complessità anche se si è in CNF; seppure con 3 variabili per clausola (3-CNF), in espressioni del tipo:

(x₁₁ OR x₁₂ OR x₁₃) AND

(x₂₁ OR x₂₂ OR x₂₃) AND

(x₃₁ OR x₃₂ OR x₃₃) AND ...

dove ogni x è una variabile o la negazione di una variabile, e ogni variabile può apparire più volte nell'espressione della formula.

Una proprietà utile della riduzione proposta da Cook è che l'insieme delle soluzioni (assegnamenti) non viene ridotto di numero. Se ad esempio un grafo ha 17 valide 3-colorazioni, la SAT formula prodotta ne avrà ancora 17.

[modifica] 2-soddisfacibilità

Per approfondire, vedi la voce 2-soddisfacibilità.

Il problema SAT è più semplice se le formule sono limitate alla DNF, forma normale cosiddetta disgiuntiva, dove cioè le clausole sono AND di letterali (eventualmente negati) e sono combinate in OR fra di loro. Tale forma normale è la duale della CNF, e una formula in DNF è ancora soddisfacibile se e solo se almeno una delle sue clausole lo è; perché ciò avvenga, una clausola non deve contenere sia x che NOT x per qualche variabile x. La verifica di tale problema è effettuabile in tempo polinomiale.

SAT è ovviamente più semplice se il numero dei lettereali per clausola è limitato a massimo 2, e in tal caso il problema è, come detto, 2SAT. Anch'esso risolvibile in tempo polinomiale, e completo per la classe NL, tale problema può essere ulteriormente trasformato modificando i connettivi AND con XOR, creando un or-esclusivo 2-soddisfacibilità, problema completo per la classe SL = L.

Una delle più importanti restrizioni di SAT è HORNSAT, dove le formule sono congiunzioni di clausole Horn. Il problema è risolvibile in tempo polinomiale dall'algoritmo Horn-soddisfacibilità ed è per questo P-completo. Può essere visto come la versione P-complessa del problema SAT.

Assunto che le classi di complessità P e NP non sono uguali, nessuna di queste riduzioni di SAT appena descritte è NP-completa. L'assunzione però che P e NP siano diseguali non è ad oggi dimostrato, e rappresenta uno dei maggiori traguardi inseguiti dai matematici di tutto il mondo.

[modifica] 3-soddisfacibilità

È un caso speciale della k-soddisfacibilità (k-SAT), dove ogni clausola contiene esattamente k = 3 letterali. Fu uno dei 21 problemi NP-completi di Karp.

Ecco un esempio, dove ~ indica l'operatore NOT:

E = (x₁ OR ~x₂ OR ~x₃) AND (x₁ OR x₂ OR x₄)

E ha due clausole (contenute fra parentesi), quattro letterali (x₁, x₂, x₃, x₄), e k=3 (tre letterali per clausola).

Poiché k-SAT (caso generale) si riduce a 3-SAT, e 3-SAT può dimostrarsi essere NP-completo, può anche essere utilizzato per provare che altri problemi lo sono. Il procedimento consiste nel mostrare che una soluzione di un altro problema può essere utilizzata per risolvere 3-SAT. Un esempio di problema in cui è stato utilizzato tale metoto è il Problema Clique. Spesso è più facile utilizzare riduzioni da 3-SAT che da SAT stesso per provare che certi problemi siano NP-completi.

[modifica] Estensioni di SAT

Un'estensione che ha guadagnato una certa popolarità dal 2003 è stata la Satisfiability modulo theories che può arricchire le formule CNF con vincoli lineari, vettori, vincoli all-different, funzioni non interpretate, ecc. Queste estensioni, tipicamente, restano NP-complete; alcuni risolutori efficienti hanno tuttavia la capacità di maneggiarli come fossero semplici vincoli.

Il problema della soddisfacibilità sembra diventare più difficile (PSPACE-completo) se permettiamo l'utilizzo di quantificatori come "per ogni" o "esiste qualche" che operano sulle variabili booleane. Un esempio di tali espressioni potrebbe essere:

Se utilizziamo esclusivamente il quantificatore , siamo ancora di fronte al problema SAT. Se permettiamo invece solamente l'uso del quantificatore , diventa un problema Co-NP-completo tautologico. Se permettiamo l'uso di entrambi, prende il nome di problema su formule booleane quantificate (QBF), che si dimostra essere PSPACE-completo. È largamente diffusa l'opinione che tali problemi siano strettamente più difficili di qualsiasi NP, sebbene la dimostrazione di tale fatto non sia stata mostrata.

Esiste un numero di varianti del problema che riguardano la numerosità degli assegnamenti di variabili che rendono la formula vera. Il SAT ordinario chiede solamente che ne esista almeno uno; MAJSAT, che richiede che la maggioranza di tutti gli assegnamenti la renda vera, è completo per PP, classe probabilistica. Il problema di quanti assegnamenti soddisfino una data formula non è un problema decisionale, e si trova in #P. UNIQUE-SAT or USAT è invece il problema di determinare quando una formula, nota per avere o uno o nessun assegnamento che la soddisfa, ne ha uno o zero, appunto. Sebbene questo problema possa apparire più semplice è stato dimostrato che se esiste un algoritmo (randomizzato tempo polinomiale) che risolve tale problema, allora tutti i problemi in NP si possono risolvere con la stessa facilità.

Il problema di massima soddisfacibilità, una generalizzazione FNP di SAT, chiede il massimo numero di clausole che possono essere soddisfatte da ogni assegnamento. Esistono dei buoni algoritmi che lo approssimano efficientemente, ma è NP-hard risolverlo esattamente. Fattore ancora più scoraggiante, è anche un problema APX-completo e cioè non esiste un'approssimazione tempo polinomiale per questo problema a meno che non sia dimostrato che P=NP!

[modifica] Algoritmi di risoluzione di SAT

Ci sono due classi di algoritmi ad alte prestazioni che risolvono istanze del problema SAT: varianti moderne dell'algoritmo DPLL, come l'algoritmo Chaff o il GRASP, e algoritmi di ricerca locale stocastica come il WalkSAT.

Un risolutore SAT DPLL utilizza sistematicamente la procedura di backtracking ai fini dell'esplorazione dello spazio degli assegnamenti delle variabili (eventualmente di grandezza esponenziale), cercando assegnamenti che soddisfino la formula. Le basi della procedura di ricerca fu proposta nei primi anni '60 in due lavori che sono oggi noti come parte dell'algoritmo Davis-Putnam-Logemann-Loveland (DPLL). I moderni risolutori SAT, sviluppati negli ultimi dieci anni, arricchiscono quei concetti con procedure di analisi dei conflitti, apprendimento clausale, backtracking non cronologico (anche noto come backjumping), propagazione lineare, adaptive branching e riavvii random. Si è dimostrato che queste aggiunte al funzionamento di base sono state necessarie per poter maneggiare le più grandi istanze di SAT, sopraggiunte nello studio teorico in campi come l'intelligenza artificiale, ricerca operazionale, e altri. Alcuni potenti risolutori sono di pubblico dominio; in particolare MiniSAT, vincitore della competizione SAT nell'anno 2005, è formato di sole 600 linee di codice.

Algoritmi genetici e altre procedure di applicazione generale sono state utilizzate per risolvere problemi SAT, specialmente in presenza di limitate (o addirittura assenti) conoscenze della struttura specifica dell'istanza del problema da risolvere. Alcuni tipi di corpose istanze casuali (soddisfacibili) del SAT si possono risolvere con la Survey Propagation (SP).

[modifica] Note

1. D. Babić, J. Bingham, and A. J. Hu, "B-Cubing: New Possibilities for Efficient SAT-Solving", IEEE Transactions on Computers 55(11):1315–1324, 2006.
2. R. E. Bryant, S. M. German, and M. N. Velev, "Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions," in Analytic Tableaux and Related Methods, pp. 1-13, 1999.
3. E. Clarke, A. Biere, R. Raimi, and Y. Zhu, "Bounded Model Checking Using Satisfiability Solving," Formal Methods in System Design, vol. 19, no. 1, 2001.
4. S. A. Cook, "The Complexity of Theorem Proving Procedures," in Proc. 3rd Ann. ACM Symp. on Theory of Computing, pp. 151-158, Association for Computing Machinery, 1971.
5. M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," Journal of the Association for Computing Machinery, vol. 7, no., pp. 201-215, 1960.
6. M. Davis, G. Logemann, and D. Loveland, "A Machine Program for Theorem-Proving," Communications of the ACM, vol. 5, no. 7, pp. 394-397, 1962.
7. N. Een and N. Sorensson, "An Extensible SAT-solver," in Satisfiability Workshop, 2003.
8. Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, 1979. ISBN 0-7167-1045-5 A9.1: LO1 – LO7, pp.259 – 260.
9. G.-J. Nam, K. A. Sakallah, and R. Rutenbar, "A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 6, pp. 674-684, 2002.
10. J. P. Marques-Silva and K. A. Sakallah, "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers, vol. 48, no. 5, pp. 506-521, 1999.
11. J.-P. Marques-Silva and T. Glass, "Combinational Equivalence Checking Using Satisfiability and Recursive Learning," in Proc. Design, Automation and Test in Europe Conference, pp. 145-149, 1999.
12. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: engineering an efficient SAT solver," in Proc. 38th ACM/IEEE Design Automation Conference, pp. 530-535, Las Vegas, Nevada, 2001.
13. M. Perkowski and A. Mishchenko, "Logic Synthesis for Regular Layout using Satisfiability," in Proc. Intl Workshop on Boolean Problems, 2002.

[modifica] Collegamenti esterni

Risolutori SAT:

• HyperSAT
• Spear
• The MiniSAT Solver
• UBCSAT

Pubblicazioni/Conferenze:

• SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing
• Journal on Satisfiability, Boolean Modeling and Computation
• Survey Propagation

Benchmarks:

• Forced Satisfiable SAT Benchmarks
• IBM Formal Verification SAT Benchmarks
• SATLIB
• Software Verification Benchmarks

Risolutori SAT in generale:

• http://www.satlive.org
• http://www.satisfiability.org
• Sat4j

Questo articolo contiene estratti da: SIGDA e-newsletter del Prof. Karem Sakallah
Il testo originale è disponibile a questo indirizzo.