Soddisfacibilità booleana

La soddisfacibilità booleana, o soddisfacibilità proposizionale o SAT, è il problema di determinare se una formula booleana è soddisfacibile o insoddisfacibile. La formula si dice soddisfacibile se le variabili possono essere assegnate in modo che la formula assuma il valore di verità vero. Viceversa, si dice insoddisfacibile se tale assegnamento non esiste (pertanto, la funzione espressa dalla formula è identicamente falsa).

Il problema di determinare la soddisfacibilità booleana

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

La domanda è la seguente: data un'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. Il problema SAT è di importanza centrale in molte aree dell'informatica, incluse l'informatica teorica, lo studio degli algoritmi, la progettazione dell'hardware, ecc.

Senza perdita di generalità, il problema può essere ricondotto al caso particolare in cui la formula è espressa in forma normale congiuntiva (CNF), ovvero come un AND di clausole ognuna formata da un OR di letterali. Infatti, applicando i Teoremi di De Morgan, si può ricondurre la formula al caso in cui gli operatori NOT sono applicati solo alle variabili, e non alle 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.

Il teorema di Cook-Levin dimostra che il problema di determinare se una qualunque formula proposizionale è soddisfacibile è NP-completo. Ad esempio, è NP-completo (e prende il nome di "3SAT", "3CNFSAT", o "3-soddisfacibilità") il problema di determinare la soddisfacibilità di una formula in cui ogni clausola ha un massimo di tre letterali. Tuttavia, se restringiamo ogni clausola ad avere massimo due letterali, allora il problema risultante, detto 2SAT, è NL-completo. Determinare la soddisfacibilità di una formula in cui ogni clausola è una clausola di Horn (cioè contiene al massimo un letterale positivo) è un problema P-completo e prende il nome di Horn-soddisfacibilità.

SAT è stato il primo problema decisionale di cui si è dimostrata la NP-completezza. Nonostante ciò, nell'ultimo decennio si sono fatti enormi passi avanti, individuando algoritmi scalabili per risolvere SAT con decine di migliaia di variabili e milioni di vincoli. Esempi di questi problemi sono presenti in model checking, Electronic Design Automation (EDA), FPGA, sintesi logica, ecc..

Complessità

NP-completezza

Prima del 1971 e del Teorema di Cook-Levin 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 (assegnazioni) non viene ridotto di numero. Se ad esempio un grafo ha 17 valide 3-colorazioni, la SAT formula prodotta ne avrà ancora 17.

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 letterali 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 dimostrata, e rappresenta uno dei maggiori traguardi inseguiti dai matematici di tutto il mondo.

3-soddisfacibilità

È un caso speciale della k-soddisfacibilità (k-SAT), dove ogni clausola contiene al più 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 metodo è il problema della cricca. Spesso è più facile utilizzare riduzioni da 3-SAT che da SAT stesso per provare che certi problemi siano NP-completi.

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:

\forall x,\exists y,\exists z;(x\lor y\lor z)\land (\lnot x\lor \lnot y\lor \lnot z)

Se utilizziamo esclusivamente il quantificatore $\exists$ , siamo ancora di fronte al problema SAT. Se permettiamo invece solamente l'uso del quantificatore $\forall$ , diventa un problema Co-NP-completo di individuare se la forma risulta essere una tautologia. 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!

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).

Note

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.
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.
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.
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.
M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," Journal of the Association for Computing Machinery, vol. 7, pp. 201–215, 1960.
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.
N. Een and N. Sorensson, "An Extensible SAT-solver," in Satisfiability Workshop, 2003.
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.
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.
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.
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.
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.
M. Perkowski and A. Mishchenko, "Logic Synthesis for Regular Layout using Satisfiability," in Proc. Intl Workshop on Boolean Problems, 2002.

Altri progetti

Wikimedia Commons contiene immagini o altri file sulla soddisfacibilità booleana

Collegamenti esterni

(EN) satisfiability problem, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.

(EN) Eric W. Weisstein, Soddisfacibilità booleana, su MathWorld, Wolfram Research.

Risolutori SAT:

HyperSAT, su cs.ubc.ca.
Spear, su cs.ubc.ca.
The MiniSAT Solver, su minisat.se.

Pubblicazioni/Conferenze:

SAT 2007: Tenth International Conference on Theory and Applications of Satisfiability Testing, su sat07.ecs.soton.ac.uk.
Journal on Satisfiability, Boolean Modeling and Computation, su jsat.ewi.tudelft.nl. URL consultato il 6 maggio 2019 (archiviato dall'url originale il 19 febbraio 2006).
Survey Propagation, su ictp.trieste.it. URL consultato il 26 marzo 2007 (archiviato dall'url originale il 10 febbraio 2006).

Benchmarks:

Forced Satisfiable SAT Benchmarks, su nlsde.buaa.edu.cn. URL consultato il 26 marzo 2007 (archiviato dall'url originale il 25 gennaio 2021).
IBM Formal Verification SAT Benchmarks, su haifa.il.ibm.com. URL consultato il 26 marzo 2007 (archiviato dall'url originale il 17 luglio 2007).
Software Verification Benchmarks, su cs.ubc.ca.

Risolutori SAT in generale:

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

Portale Informatica

Portale Matematica