1

Il Problema 3SAT

Rosario Turco

Il 3SAT è un problema decisionale di "soddisfacibilità booleana" (logica binaria o SAT), dove si vogliono trovare le

soluzioni di una funzione logica, costituita da AND di clausole, dove una clausola è però costituita da due OR di 3

letterali e in gioco vi sono n variabili con n>3.

In altri termini ad esempio per n=4 variabili A1,A2,A3,A4 abbiamo clausole costituite dall'OR con sole 3 variabili (o

combinazioni di NOT e/o variabili) e tutte le clausole scelte sono poi in AND.

Le soluzioni sono tutte quelle ottenute, tenendo conto dei valori assunti dalle variabili (condizioni iniziali), mettendo

prima in OR i valori di 3 letterali di una clausola e infine mettendo in AND le varie clausole assegnate, e che

comportano alla fine che la funzione logica valga TRUE. Le clausole si dicono in forma normale congiuntiva (CNF).

Ciò comporta che:

1) può esistere o meno la soluzione costituita da tutte le variabili (esistono delle clausole che vanno scartate o che se

usate comportano che la funzione logica dà come risultato FALSE).

Ad esempio supponiamo il problema n=4, alcune soluzioni non utili per la funzione sono:

A1 A2 A3 A4 FUNZIONE LOGICA FALSE PER LA SOLUZIONE

1 1 1 1 AND(OR(OR(NOT(A1),NOT(A2)),NOT(A3)),OR(OR(A1,A2),A4)

0 0 1 0 AND(OR(OR(A1,A2),A3),OR(OR(A1,A2),A4))

A1 A2 A3 A4 FUNZIONE LOGICA TRUE PER LA SOLUZIONE

0 0 0 1 AND(OR(OR(NOT(A1),NOT(A2)),NOT(A3)),OR(OR(A1,A2),A4)

Ovviamente la stessa funzione per una configurazione di valori dei letterali risulta falsa e per un’altra vera; in altri casi

può essere addirittura sempre falsa, ovvero non ammette soluzione.

Per cui sono possibili vari tipi di problemi:

a) assegnata la funzione logica trovare le soluzioni

b) assegnata una soluzione quali clausole devono essere scartate per non dare FALSE nella funzione logica

c) se è possibile minimizzare la funzione logica in taluni casi, il che vuol dire che alcune clausole potrebbero essere

ininfluenti o che la funzione logica è invariante rispetto a inserire o togliere certe clausole.

In sostanza sono, quindi, importanti le minimizzazioni della funzione logica e l'esistenza della soluzione.

In generale esistono molti metodi di minimizzazione tra cui quello degli Implicanti primi (Quine-McCluskey) o più

semplicemente le mappe di Karnaugh. Le mappe di Karnaugh hanno un limite di utilizzabilità pratica appena il

numero dei letterali in gioco supera 4-5 diventano poco facili a gestirsi; mentre il metodo degli implicanti Primi (vedi

[1]) gestisce meglio n variabili, ma risolvendo un problema NP-difficile il tempo di esecuzione è esponenziale al

crescere dei letterali.

L’interesse per i problemi SAT, 2SAT, 3SAT è nato col Teorema di Cook e Levin (vedi [4]), che afferma che il problema della soddisfacibilità booleana è NP-complete. Il che vuol dire che un problema in NP può essere ridotto in un tempo polinomiale con una macchina di Turing deterministica se una formula booleana è soddisfacibile. SAT fu proprio il primo problema che fu dimostrato da Cook come NP-difficile. Ovviamente ne esistono molti altri problemi come quello dello zaino, etc.

2

La conseguenza del teorema è che se esiste un algoritmo deterministico in tempo polinomiale per risolvere il problema della soddisfacibilità booleana, allora esiste un algoritmo deterministico in tempo polinomiale per risolvere tutti i problemi in NP. Lo stesso segue da ogni problema NP complete. In poche parole la questione se esiste un algoritmo del genere è un altro problema del millennio noto come problema informatico. Dimostrare che esiste equivale a dimostrare che P=NP (vedi [2][3][5][6]).

Il problema 3SAT è NP-completo. Se n sono le variabili e indichiamo con c l'intero maggiore o uguale a n/3, allora per

ottenere una soluzione minima nel 3SAT, servono almeno c partizioni diverse di clausole che contengano tutte le

variabili.

Se indichiamo con p i partizionamenti di clausole, ad esempio se m=2^3=8 T=32 p=4, ovvero abbiamo almeno 4

famiglie di clausole in gioco indipendentemente dai valori dei letterali:

Partizione Letterali

P1 A1+A2+A3

P2 A1+A2+A4

P3 A1+A3+A4

P4 A2+A3+A4

La funzione logica minima richiede, in questo caso, almeno c= ceil(4/3) = 2 partizioni che contengano tutte le n

variabili (ad esempio p1 e p2).

Sopra col + intendiamo l'OR e p1 indica ad esempio il primo partizionamento che contiene i letterali A1, A2 e A3.

Inoltre per ogni partizionamento pi si possono avere i seguenti "accoppiamenti non ripetuti":

p1-p2,p1-p3,p1-p4

p2-p3,p2-p4

p3-p4

In totale, per l'esempio, ci sono 6 accoppiamenti di partizioni, equivalenti in generale a (p-1)!. Mentre se p è il n.ro di

partizionamenti, allora la singola partizione pi ha (p-i) accoppiamenti non ripetuti rispetto ai pi precedenti.

La tabella dell'insieme totale delle clausole di 3 Letterali è costituita da un numero calcolabile con

T = D2,n * Cn,3 = 2^n * binomial(n,3)

dove D2,n sono le disposizioni di 2 valori su n posti e Cn,3 è la combinazione di n variabili raggruppate a 3 alla volta.

Minimizzazione del 3SAT

Se n è il numero di letterali, F è la funzione logica del 3SAT, Cmtl il numero di clausole minime con tutti i letterali, C il

numero di clausole che presenta F e con Cmtl = ceil(n/3), allora se C > Cmtl ci sono delle clausole che si potrebbero

eliminare e, quindi, si deve verificare se è possibile minimizzare la funzione logica F di partenza.

Metodo di minimizzazione dei letterali del 3SAT (metodo esaustivo esponenziale)

Se C > Cmtl la verifica si effettua nel seguente modo:

1 si individua un numero di clausole uguale a Cmtl dove siano presenti tutti i letterali.

2 Per ogni clausola ulteriore a quelle Cmtl selezionate, sottolineare in esse i letterali ripetuti (per letterale ripetuto si

intendono i letterali identici per verità o negazione. Ad esempio A è identico solo ad A, NOT(A) è identico solo a

NOT(A).

3

3 Se tutti i letterali di una clausola sono sottolineati, la clausola va eliminata perché è “non influente”, ma va eliminata

eventualmente anche la soluzione che la renderebbe Falsa.

4 Se almeno uno dei letterali di una clausola è sottolineato (ma non tutti), la clausola non va eliminata perché è

“influente”.

Il numero di operazioni ridotte nella ricerca di soluzioni esaustiva è di 3*2^N dove N è il numero dei letterali; inoltre di

ogni clausola non è detto che vengono esaminati tutti i letterali, grazie ad delle “Accelerator rules”, nel caso peggiore

si esaminano tutti, ma mediamente ciò non accade su tutte le clausole.

In totale se le clausole della funzione logica sono Q, se Qr sono le clausole eliminate per minimizzazione, allora tutte le

operazioni da fare sono:

Q * 3 * 2^N – Qr * 3 * 2^N = 3 * 2^N * (Q - Qr)

A questo sarebbe possibile aggiungere un fattore moltiplicativo K, variabile tra 0,3 e 1,0 per gli Accelerator.

Ovviamente all’aumentare di N, numero dei letterali, maggiore è il tempo di elaborazione, di memoria in gioco etc.

Esempio:

N=4 Letterali A1, A2, A3, A4

F=(A1+A2+A3)*(NOT(A1)+NOT(A2)+A4)*(A1+A3+A4)*(A2+A3+A4)

C=4

Cmtl = 2 =ceil(4/3) -> scegliamo (A1+A2+A3)*(A1+A3+A4) che rispettano Cmtl e contengono tutti i letterali

Minimizzazione dei letterali

F=(A1+A2+A3)* (A1+A3+A4)*(NOT(A1)+NOT(A2)+A4)*(A2+A3+A4)

La parte in rosso si elimina, si eliminano anche le soluzioni X000 con X=0 o X=1 e la funzione logica è equivalente a:

Fm=(A1+A2+A3)* (A1+A3+A4)*(NOT(A1)+NOT(A2)+A4)

Il risultato di verità (T) di F e Fm conferma che sono equivalenti. Ad esempio se A1=T, A2=T, A3=T, A4=T è F=T e Fm=T.

La Fm riduce almeno due operazioni di OR ed una di AND, per tutte le configurazioni possibili di valori dei letterali che

sono pari a 2^N, quindi in totale elimina 3*2^N “operazioni ininfluenti”. In più si possono aggiungere delle

“Accelerator rules” sull’or: “basta un letterale a 1 in una clausola per passare alla clausola successiva” e sull’and: “al

primo and nullo è inutile verificare la configurazione di soluzione considerata”.

Questo metodo è anche semplice a implementarsi con un algoritmo, basandosi su uno “stack di marcatura” parallelo a

quello dei letterali totali (che esclude però le clausole scelte di Cmtl), che mette a zero quelli eventualmente

eliminabili, se tutte le terne (a tre a tre) sono nulle si elimina la clausola corrispondente, mente se uno solo dei

letterali non è marcato a zero la terna dei letterali rende la “clausola influente”.

Metodo delle Mappe di Karnaugh o degli Implicanti primi

Le mappe di Karnaugh sono adatte a funzioni logiche del tipo A NOT(B) C + NOT(A) B C, funzioni logiche caratterizzate

dall’AND dei letterali e con il risultato in OR. Tuttavia applicando il Teorema di De Morgan ci si può ricondurre da un

problema 3SAT ad uno identico trattabile con le mappe di Kaurnaugh, ad esempio per una clausola:

NOT(A B C ) = NOT(A) + NOT(B) + NOT(C)

4

Esempio

F=(A1+A2+A3)* (A1+A3+A4)*(NOT(A1)+NOT(A2)+A4)*(A2+A3+A4)

Consideriamo la funzione NOT(F), se essa è falsa allora F è vera. Per cui col Teorema di De Morgan è:

NOT(F) = (NOT(A1) NOT(A2) NOT(A3)) + (NOT(A1) NOT(A3) NOT(A4)) + (A1 A2 NOT(A4)) + (NOT(A2) NOT(A3) NOT(A4))

Su SAT, 2SAT e 3SAT esistono molti algoritmi deterministici, evolutivi, probabilistici (vedi [7][8]). Il problema

fondamentale è una dimostrazione che P=NP, che è il vero problema finale a cui tendono i vari casi

References

[1] http://it.wikipedia.org/wiki/Metodo_di_Quine-McCluskey

[2] http://www.win.tue.nl/~gwoegi/P-versus-NP.htm

[3] Stephen Cook -The P versus NP Problem -

http://www.claymath.org/millennium/P_vs_NP/Official_Problem_Description.pdf

[4] http://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem

[5] Wikipedia - Karp's 21 NP-complete problems http://en.wikipedia.org/wiki/Karp's_21_NPcomplete_problems

[6] http://en.wikipedia.org/wiki/P_%3D_NP_problem

[7] http://it.wikipedia.org/wiki/Algoritmo_di_Davis-Putnam

[8] http://it.wikipedia.org/wiki/DPLL