Data una formula logica, sappiamo che l’algoritmo SAT risolve il problema della soddisfacibilità booleana. In poche parole l’algoritmo determina se la formula logica può essere resa vera da un’appropriata assegnazione di valori di verità (vero o falso) alle sue variabili.
SAT è il primo problema per cui è stata dimostrata la completezza NP da Stephen Cook nel 1971. Appartiene alla classe dei problemi NP (risolvibili in tempo polinomiale da una macchina di Turing non deterministica), quindi ogni problema in NP può essere trasformato in un problema SAT in tempo polinomiale.
G-SAT è la versione greedy di SAT. Vediamo in dettaglio come funziona.
Cos’è G-SAT
Essendo la versione greedy (avida) dell’algortimo, G-SAT cerca di ottimizzare le scelte in modo avido considerando la scelta locale ottima.
Si tratta di un algoritmo incompleto in quanto non utilizza tutto lo spazio di ricerca a disposizione. Questo potrebbe causare dei falsi negativi, in quanto nonostante una formula possa essere soddisfacibile, l’algoritmo non è in grado di trovare per essa un assegnamento che la renda tale.
Prima di proseguire vorrei semplicemente dirti che il mio è un progetto di divulgazione, se ti piacciono i miei contenuti e ti va di sostenermi unisciti al mio canale Telegram oppure consulta le mie guide all’acquisto.
Come funziona G-SAT
La premessa da sapere prima di utilizzare G-SAT è che stiamo considerando formule in forma CNF, ovvero Conjunctive Normal Form (la congiunzione è determinata dall’operatore logico AND). Ad esempio:
( x1 ∨ x2 ) ∧ ( ¬x2 ∨ x3 ∨ ¬x4 ) ∧ ( x4 ∨ ¬x1 )
Dove:
- I letterali sono x1, x2, x3 e x4;
- Le clausole sono gli OR (disgiunzioni) dei letterali:
- ( x1 ∨ x2 )
- ( ¬x2 ∨ x3 ∨ ¬x4 )
- ( x4 ∨ ¬x1 )
Se hai una formula specifica su cui applicare G-SAT ma non è in forma CNF allora tramite le varie tecniche che mantengono la sua equivalenza logica puoi convertire il formato e poi applicare l’algoritmo.
Inoltre, l’algoritmo fa uso di una funzione obiettivo, come funziona? Data la formula F, l’assegnamento x e la funzione sat(F, x) che restituisce il numero di clausole di F soddisfatte da x. La funzione obiettivo è max(sat(F, x)).
Passi dell’algoritmo G-SAT
A questo punto posso descrivere il funzionamento dell’algoritmo:
Viene fissato un numero di iterazioni totali che l’algoritmo può fare. All’interno di ogni iterazione viene inizialmente generato un assegnamento randomico delle variabili presenti all’interno della formula.
Se l’assegnamento rende soddisfacibile la formula, l’algoritmo termina. Altrimenti vengono generati i vicini dell’assegnamento corrente (per vicini si intendono tutte le combinazioni che differiscono di un solo bit dall’assegnamento corrente, quindi se le variabili sono n anche il vicinato ha dimensione n).
Se viene trovato un vicino che ottimizza la funzione obiettivo (passo greedy), questo diventa il nuovo assegnamento corrente e quindi si ripete il procedimento, ovvero se questo non rende la formula soddisfacibile vengono generati i vicini e così via.
Altrimenti se non c’è nessun vicino che ottimizza la funzione obiettivo si riparte con una nuova iterazione (che prende il nome di passo di restart).
Di seguito, ecco una bozza dell’algoritmo G-SAT in Python.
import random
def assegna_random(n_vars):
""" Assegna valori booleani casuali alle variabili. """
return [random.choice([True, False]) for _ in range(n_vars)]
def calcola_vicini(assegnamento):
""" Genera vicini invertendo una variabile alla volta. """
vicini = []
for i in range(len(assegnamento)):
nuovo_assegnamento = assegnamento[:]
nuovo_assegnamento[i] = not nuovo_assegnamento[i]
vicini.append(nuovo_assegnamento)
return vicini
def funzione_obiettivo(assegnamento):
""" Valuta quanti clausole vengono soddisfatte dall'assegnamento. """
# Questa funzione deve essere definita in base alla specifica formula CNF
return sum(assegnamento) # Esempio semplice che conta il numero di True
def gsat(max_tries, n_vars):
iterazione = 0
assegnamento_corrente = None
while iterazione < max_tries:
assegnamento_corrente = assegna_random(n_vars)
if assegnamento_corrente: # Verifica se l'assegnamento è valido
if funzione_obiettivo(assegnamento_corrente) == n_vars:
return assegnamento_corrente
vicini = calcola_vicini(assegnamento_corrente)
miglior_vicino = max(vicini, key=funzione_obiettivo)
if funzione_obiettivo(miglior_vicino) > funzione_obiettivo(assegnamento_corrente):
assegnamento_corrente = miglior_vicino
continue # Ricomincia il ciclo while senza incrementare iterazione
iterazione += 1
return assegnamento_corrente