Implementazione della procedura DPLL

attraverso il linguaggio di programmazione JAVA

La procedura DPLL è considerata il metodo computazionalmente più efficiente per valutare se una formula proposizionale S sia soddisfacibile o meno; l'istanza di ingresso della procedura è rappresentata da un insieme di clausole ground (ovvero un insieme dove non appaiono variabili ma solo letterali) in forma normale congiunta (CNF), mentre l'output consiste nel decidere se l'insieme sia soddisfacibile o meno, nel caso in cui lo sia l'algoritmo restituisce un assegnamento che soddisfa l'insieme di clausole.
Quindi, a partire da una formula si cerca di costruire un assegnamento che la verifichi; la procedura può essere vista come un albero di possibili assegnamenti nel quale ciascun nodo rappresenta un insieme di clausole e per ogni nodo ad un letterale viene assegnato un valore di verità; tale valore viene poi propagato per ridurre il numero di assegnamenti futuri.
Un ramo dell'albero non viene più espanso se l'insieme di clausole è vuoto (S è soddisfacibile) oppure se è stata generata la clausola vuota (S è non soddisfacibile). Gli assegnamenti vengono effettuati applicando alcune regole che preservano la soddisfacibilità:

• Tautology Elimination: dall'insieme di clausole vengono eliminate le istanze ground che sono tautologie
• One Literal: se esiste una clausola unitaria LЄS, otteniamo S' da S eliminando quelle clausole ground in S che contengono L. Se S={} allora S è soddisfacibile altrimenti otteniamo un insieme S" da S' eliminando ¬L da tutte le clausole; S è non soddisfacibile se e solo se S" è non soddisfacibile. Quando applichiamo questa regola fissiamo L=Τ nell'assegnamento parziale
• Pure Literal: LЄS è un letterale puro se ¬L non appartiene ad S, se esiste tale letterale allora otteniamo S' rimuovendo tutte le clausole dove appare L (quando questa regola viene applicata, fissiamo L=Τ nell'assegnamento parziale)
• Splitting Rule: se possiamo scrivere S nella forma S = (C₁ ∨ L) ∧ ... ∧ (C_m ∨ L) ∧ (D₁ ∨ ¬L) ∧ ... ∧ (D_m ∨ ¬L) ∧ S_r dove C_i e D_i sono clausole in cui L e ¬L non appaiono e dove S_r è un insieme di clausole dove L e ¬L non appaiono, allora possiamo ottenere due insiemi S'=C₁ ∧ ... ∧ C_m ∧ S_r e S"=D₁ ∧ ... ∧ D_m ∧ S_r. L'insieme S è non soddisfacibile se e solo se S' e S" sono non soddisfacibili. Quando questa regola viene applicata, viene eseguito uno split dell'albero degli assegnamenti e fissiamo L=Τ per il ramo di S" e L=F per il ramo di S'.

Il linguaggio di programmazione scelto per l'implementazione del progetto è JAVA, versione 1.6.0.
La classe Dpll() che implementa la procedura DPLL inizialmente deve leggere l'insieme di clausole da un file costruito seguendo un formato standard così definito: il file inizia con un'intestazione rappresentata dalla seguente linea

p cnf num_lett num_cla

dove num_lett indica il numero di lettere proposizionali che occorrono nella formula e num_cla indica il numero delle clausole presenti nella formula; ogni linea che inizia con la lettera c viene considerata un commento. Gli atomi sono espressi con numeri da 1 a num_lett; la negazione di un atomo è rappresentata da un numero negativo. Una clausola è invece rappresentata da una riga di letterali separati tra loro da uno spazio e terminante con uno 0. Un esempio di formula sarà descritta dal seguente file:

c *** insoddisfacibile ***
p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0


Inizialmente, quindi, viene aperto uno stream in lettura di un file avente la forma appena menzionata, ogni riga di tale stream viene convertita in stringa e, attraverso il metodo num_lit(), viene fatto uno scorrimento delle stringhe corrispondenti a ciascuna riga fino a che il primo carattere letto corrisponda al carattere p, in questo caso vengono ricavati due interi corrispondenti al numero di lettere proposizionali che occorrono e al numero di clausole presenti nella formula; poi, finché sono presenti dell righe da leggere dal file, viene memorizzato il numero totale di atomi presenti nella formula. Queste tre informazioni vengono inserite in un array di interi, che viene restituito dal metodo; poi, attraverso il metodo create_clause(), viene fatto uno scorrimento dello stream fino a che il primo carattere letto di una riga sia diverso dai caratteri c e p, ciò significa che la sequenza di valori numerici corrispondenti ad atomi della formula ha inizio e quindi ogni intero incontrato viene inserito in un array.
L'operazione successiva consiste nel creare, a partire dall'array statico appena definito, un array di liste sul quale poi verranno eseguite le quattro regole viste in precedenza. L'idea, quindi, è quella di avere un array, avente dimensione statica pari al numero di clausole, di liste. L'informazione relativa all'insieme di clausole iniziali comunque non viene persa, visto che rimane memorizzata nell'array statico definito dal metodo create_clause() e che non viene mai modificato durante l'esecuzione.
Poi viene invocato il metodo taut_check() che si occupa di verificare se, nell'insieme di clausole, sono presenti delle tautologie: in caso affermativo, viene eliminata la clausola, ovvero la lista, che contiene la tautologia.
Il passo seguente è quello di identificare se esiste un letterale unitario: il metodo one_literal() va a scorrere l'array di liste, quando ne trova una unitaria questa viene rimossa la lista; se invece non ne trova, restituisce 0. Oltre a rimuovere la lista, il metodo one_literal() restituisce anche il letterale individuato visto che quest'informazione è necessaria per l'operazione successiva: infatti viene invocato il metodo unit_clause() che si occupa di cercare, nelle altre liste, se è presente il letterale opposto a quello unitario; se viene trovato, attraverso il metodo remove(i) fornito dalla classe ArrayList() è possibile eliminare l'i-esimo carattere della lista, il quale rappresenta il letterale unitario negato. Inoltre, l'intero corrispondente al letterale unitario viene inserito in una lista che conterrà uno dei possibili modelli che verranno individuati dalla procedura, nel caso in cui la formula risulti soddisfacibile.
Al termine di questi passi viene applicata la regola Pure Literal: il metodo pure_literal() va a scorrere l'insieme di clausole e, per ciascun letterale, viene invocato il metodo isPure(); tale funzione controlla se nelle altre liste è presente o meno il corrispondente letterale negato, in caso affermativo la procedura prosegue il controllo sugli altri letterali, in caso negativo allora significa che è presente un letterale puro perciò viene rimossa la lista che contiene tale letterale, il quale viene inserito nella lista che memorizza il modello.
Al termine dell'esecuzione delle tre regole (Tautology Elimination, One Literal, Pure Literal) viene eseguito un controllo sulla dimensione delle liste per capire se ci sono ancora letterali presenti: se tutte le liste sono vuote, allora siamo riusciti a determinare se la formula è soddisfacibile o meno, altrimenti viene invocato il metodo split().
In questo metodo innanzitutto viene creata una lista che è la copia di quella (passata come parametro) che contiene tutte le clausole della formula, questo perché nel caso in cui lo split non andasse a buon fine con il letterale scelto (ovvero la formula risultasse non soddisfacibile), la procedura andrà ripetuta con il letterale opposto sullo stesso array di liste. Poi viene scelto il letterale su cui effettuare lo split invocando il metodo choose_var(), che, per ogni letterale, va a contare il numero di volte in cui esso è presente nella formula; quello che compare maggiormente sarà il letterale scelto per lo split, in questo modo si cerca di ridurre il più possibile il numero di clausole da controllare nei passi successivi della procedura. Tale letterale poi viene inserito nella lista che descrive il modello.
L'operazione successiva consiste nell'invocazione del metodo check_sat(): questo metodo va ad eseguire una procedura ricorsiva che verifica se il ramo intrapreso scegliendo il letterale per lo split porterà ad una soluzione o meno per l'insieme di clausole; nel caso in cui la procedura ritornasse il risultato di non soddisfacibilità, essa andrà ripetuta considerando come variabile di split il letterale opposto a quello scelto nell'iterazione precedente. Il metodo check_sat() prima di tutto va a scorrere l'array di liste per rimuovere le clausole (liste) che contengono il letterale su cui è stato deciso di effettuare lo split, ed inoltre va a rimuovere i letterali che corrispondono all'opposto dell'array su cui si sta facendo lo split; dopo di che vengono nuovamente invocati in sequenza i metodi relativi alle regole One Literal e Pure Literal. Se ci sono ancora letterali presenti nelle clausole, significa che si rende necessario un ulteriore split e quindi viene invocato nuovamente il metodo split(). Perciò, viene eseguita una procedura ricorsiva fino a che si arriva alla conclusione che l'insieme di clausole sia soddisfacibile o meno.

Il tool sviluppato è stato testato su un insieme di istanze presenti online; l'analisi dei risultati è stata fatta tenendo conto del tempo di esecuzione impiegato: grazie al metodo currentTimeMillis(), fornito dalla classe System, sono stati misurati il tempo (in millisecondi) in cui ha inizio l'esecuzione e il tempo in cui ha fine, in modo così da poter avere una misura (che verrà fornita in secondi) del tempo complessivo di esecuzione.
Sono stati raccolti due insiemi di dati: il primo che considera il caso in cui come variabile di split venga considerato il primo letterale della prima clausola (ovvero la prima lista) in cui sia presente più di un letterale; nel secondo, invece, la variabile di split viene generata dal metodo choose_var().
Come è possibile evincere dai risultati dei test, il fatto di scegliere di volta in volta il letterale "migliore" su cui effettuare lo split ha un impatto notevole sul tempo di computazione, il quale diminuisce sensibilmente sia nei casi in cui una formula risulti soddisfacibile sia in quelli in cui risulti insoddisfacibile. Inoltre, si può notare come il tempo di computazione, a parità di numero di clausole e di lettere proposizionali, sia maggiore per le formule non soddisfacibili, visto il fatto che è necessario espandere l'intero albero dei possibili assegnamenti prima e di poter affermare che una formula risulti non soddisfacibile.
In ottica di sviluppo futuro del tool, una possibile ulteriore informazione fornita potrebbe consistere nel riportare il numero di split che risultano necessari, così facendo si potrebbe arricchire l'analisi dei risultati sperimentali e legarla al tempo di esecuzione associato.