2  Procedure complete

La procedura di Davis­Putnam

Euristiche di ramificazione

Strutture di dati e la loro realizzazione

Problemi non clausolari

Backtracking intelligente ed apprendimento

Errori iniziali

Parallelization

Limiti superiori

Risoluzione

Tecniche OR

2.1     La procedura di Davis­Putnam

Nonostante la sua età e semplicità, la procedura Davis­Putnam rimane una delle migliori procedure complete per la soddisfacibilità [22]. La procedura di Davis­Putman originale [20] si basa sulla regola di risoluzione che elimina le variabili una ad una, in seguito aggiungendo tutte le soluzioni possibili alla serie di clausole. Sfortunatamente, in generale questa procedura richiede spazio esponenziale. Perciò, Davis, Logemann e Loveland hanno sostituito rapidamente la regola di risoluzione con una split rule che divide il problema in due sottoproblemi più piccoli [19]. Nella letteratura, questa procedura è chiamata imprecisamente la procedura Davis­Putnam o DP.

Figura 2.1: La procedura Davis-Putman.

Dopo l’applicazione della regola di suddivisione (split rule), semplifichiamo il set delle clausole cancellando ogni clausola che contiene il letterale l su True, spesso chiamata sussunzione di unità (unit subsumtion) e cancellando la negazione di l tutte le volte che si presenta nelle clausole rimanenti, spesso chiamata unit resolution. Notiamo che la regola sussunzione di unità può essere ignorata se la procedura DP è terminata quando ad ogni variabile è stato assegnato il valore True.

A causa del suo costo, la pure literal rule è spesso cancellata. Il modo simile alle tautologie che possono essere eliminate solamente all'inizio della ricerca, la regola tautologica è spesso cancellata. Nessuna delle due è richiesta per la correttezza o la completezza della procedura. Neanche la regola unit propagation è necessaria per la correttezza o la completezza della procedura; cosi come le split rule ed empty rule raggiungono lo stesso effetto. Comunque, la regola unit propagation contribuisce tantissimo all'efficienza della procedura Davis­Putnam. Per i problemi Horn­SAT, la regola unit propagation è la base per determinare la soddisfacibilità di una procedura completa.

Hooker ha mostrato come adattare la procedura di Davis­Putnam per determinare l’aumento della soddisfacibilità in modo efficiente [64 ]. Dato un set di clausole soddisfacenti S, il problema è di decidere la soddisfacibilità di åÈ{C} per qualche nuova clausola C.

2.2     Euristiche di ramificazione

L'algoritmo Davis­Putnam è non deterministico, poiché possiamo scegliere il letterale su cui ramificare. Una euristica di ramificazione conosciuta e conveniente è quella di Mom. Questa sceglie il letterale che si presenta più spesso nelle clausole di dimensione minima. I collegamenti di solito sono rotti con un ordine statico o casuale. In alcuni casi, calcolando il letterale che si presenta più spesso è considerato troppo costoso e si ramifica semplicemente sul primo letterale della clausola di dimensione minore.

L’euristica di Jeroslow­Wang [68] valuta il contributo che ogni letterale è probabile a far soddisfare il set di clausole. Ciascun letterale è punteggiato come segue: per ogni clausola c nella quale appare il letterale, è sommato 2^-½c½ al punteggio del letterale, dove ½c½ rappresenta il numero di letterali in c. Poi ad ogni letterale con il punteggio più alto è applicata la split rule.

Hooker e Vinay hanno investigato la motivazione riguardo la funzione punteggio utilizzata nell’euristica di Jeroslow­Wang [65]. Loro propongono l’ipotesi di soddisfazione, che è la migliore per dividerla in sottoproblemi che hanno più probabilità ad essere soddisfacibili, ma rifiutano questa in favore dell’ipotesi di semplificazione, che è la migliore per dividerla in semplici sottoproblemi con clausole più corte e più semplici dopo la unit propagation. L'ipotesi di semplificazione suggerisce una regola Jeroslow-Wang two­sided che funziona meglio della regola Jeroslow­Wang originale.

Una delle migliori realizzazioni correnti della procedura di Davis­Putnam, SATZ utilizza un’euristica basata sulla massimizzazione del numero di unit propagation [88]. Questa aggiunge un ulteriore appoggio all'ipotesi di semplificazione di Hooker e Vinay.

2.3     Strutture di dati e la loro realizzazione

Le performance della procedura di Davis­Putnam dipendono in modo critico dalla cura nella realizzazione. Crawford e Auton hanno presentato un algoritmo che fa unit resolution ed unit subsumtion in tempo lineare [ 15 ]. Per ogni variabile, ci sono liste di clausole che contengono variabili positive e negative. Ogni clausola ha un counter che contiene il numero di letterali ancora stati assegnati, ed un flag inattivo se la clausola è stata sussunta. Quando una variabile è assegnata su True, il counter delle clausole attive è decrementato quando la variabile è negativa, e quando la variabile è positiva quello delle clausole attive è messo su inattivo. Quando una variabile è assegnata su False, cambi analoghi sono compiuti. Zhang e Stickel mostrano come migliorare leggermente questo compiendo unit resolution in tempo lineare ammortizzato, ed unit subsumtion in tempo ammortizzato costante [132]. Questa modifica porta ad un miglioramento notevole dell'algoritmo di Crawford e Auton su vari problemi SAT.

Gli alberi di discriminazione (spesso chiamati tries) si sono dimostrati utili per una rapida indicizzazione in una varietà di aree di ragionamento automatizzato come la riscrittura dei vocaboli e la dimostrazione dei teoremi. Zhang e Stickel hanno comparato il loro utilizzo nella procedura di Davis­Putnam con i metodi a base di liste descritti sopra [131]. In una procedura basata su alberi di discriminazione, il set di clausole è immagazzinato come una struttura di dati ad albero i cui margini sono etichettati dai letterali, e ogni percorso rappresenta un set di letterali in una delle clausole. Unit resolution può essere compiuta poi da un'operazione di merging. I risultati sperimentali e teoretici di Zhang e Stickel suggeriscono uno schema ibrido, in cui le clausole sono rappresentate come alberi di discriminazione ma sono utilizzate liste per identificare rapidamente clausole nelle quali la variabile si presenta positiva e negativa. Questo schema è implementato nella procedura SATO [128].

2.4     Problemi non clausolari

La descrizione precedente della procedura di Davis­Putnam ha ammesso l’ipotesi che i problemi siano nella forma CNF. Questo non è essenziale. Per esempio, Otten ha usato una rappresentazione a matrice per estendere la procedura di Davis­Putnam alle formule non clausolari [100]. Esperimenti su problemi non clausolari hanno mostrato che questa procedura Davis-Putnam non clausolare esegue il suo compito meglio di una procedura Davis­Putnam standard usando la traduzione diretta nella forma clausolare (che è esponenziale nel peggiore dei casi), così come la traduzione definizionale (che è quadratica, ma introduce variabili addizionali).

2.5     Backtracking intelligente ed apprendimento

La procedura di Davis­Putnam standard compie un backtracking cronologico, esplorando completamente un ramo dell'albero di ricerca prima del backtracking e poi esplorando l'altro. Possiamo migliorare su questo adattando alcune delle migliori tecniche sviluppate dalla comunità constraint satisfaction come conflict-directed backjumping e nogood learning. Il conflict-directed backjumping percorre all’indietro l’albero di ricerca verso la causa del fallimento, ignorando gli assegnamenti irrilevanti delle variabili. Il nogood learning memorizza le cause dei fallimenti per prevenire simili errori che potrebbero essere fatti in altri rami. Bayardo e Schrag hanno descritto come gli entrambi meccanismi possono essere implementati all'interno della procedura di Davis­Putnam [4]. Loro hanno mostrato che, con questi miglioramenti (specialmente nella relevance-bounded learning), la procedura di Davis­Putnam può funzionare così bene o meglio delle migliori procedure di ricerca locale, come il GSAT ed il WalkSAT, su una larga varietà di problemi benchmark.

2.6     Errori iniziali

Un problema con una procedura completa come Davis­Putnam è che un errore iniziale può essere molto costoso. In [38], Gent e Walsh hanno identificato i problemi SAT che erano tipicamente facili ma occasionalmente potevano far fallire la procedura di Davis­Putnam. Per esempio, su un problema CP, la prima divisione ha portato immediatamente ad un sottoproblema non soddisfacibile che ha rilevato 350 milioni rami da risolvere. Nel tornare indietro verso la radice dell’albero di ricerca, è stata trovata un’istanza soddisfacente in un altro ramo senza nessuna ricerca. Gomes, Selman e Kautz hanno mostrato che una strategia di randomization e riavvii rapidi spesso possono contrastare efficacemente gli errori iniziali [54]. Meseguer e Walsh hanno mostrato che altre modifiche della strategia di ricerca depth­first come la ricerca limited discrepancy e la ricerca interleaved depth-first possono contrastano questi errori iniziali [95].

2.7     Parallelization

Le split rule non deterministiche suggeriscono un meccanismo semplice per parallelizzare la procedura di Davis­Putnam. Piuttosto che esplorare un ramo, tornare indietro, e poi esplorare l'altro, possiamo esplorare i due rami in parallelo. Comunque, dobbiamo decidere quando esplorare rami in sequenza e quando esplorarli in parallelo. Dobbiamo bilanciare anche il carico sui diversi microprocessori quanto tempo l'esplorazione di un ramo può terminare prima dell'esplorazione dell’altro. Zhang, Bonacina e Hsiang hanno perfezionato una procedura distribuita master­slave Davis­Putnam e utilizzata per risolvere problemi di esistenza dei quasigroup [130].

2.8     Limiti superiori

Sono stati dedotti vari limiti superiori per la performance della procedura Davis­Putnam e per altre procedure complete sui problemi 3SAT. Il peggiore caso di complessità temporale del Davis­Putnam è O(1.696^N), ed una piccola modifica migliora questo portandolo ad  O(1.618^N) [14]. Rodosek ha presentato un algoritmo che arriva a O(1.476^N) prendendo decisioni binarie che eliminano almeno due variabili [110].  Beigel ed Eppstein hanno presentato un algoritmo che riduce il problema 3SAT in un problema 2SAT, e poi tenta di estendere la soluzione di questo al problema originale [7]. Nel caso peggiore, questo algoritmo arriva a O(1.381^L). Comunque, quanto tempo il numero delle clausole L di solito è molto più grande del numero delle variabili N, spesso questo non rappresenta un miglioramento. Effettivamente, O(1.476^N) il limite dell'algoritmo di Rodosek è migliore per L/N=1.206.

2.9     Risoluzione

Van Gelder e Tsuji hanno migliorato la procedura di Davis­Putnam con una regola  2-closure che utilizza una versione limitata di risoluzione per generare tutti le soluzioni possibili con 2 o meno letterali [124]. Quest’algoritmo è stato molto competitivo con i problemi 3SAT random molto difficili e di analisi di circuit­fault. Più recentemente, Dechter e Rish hanno difeso la procedura di Davis­Putnam originale [21]. Loro hanno mostrato che una versione di questa procedura che loro chiamano directional resolution, lavora bene su varie classi trattabili come i problemi 2SAT così come su certi tipi di problemi strutturati. Loro hanno proposto anche una procedura approssimata, chiamata bounded directional resolution, che limita la dimensione delle soluzioni per ottenere lo spazio di complessità di tipo polinomiale. Questa procedura di approssimazione potrebbe essere utile come un passo di pre­processing per la procedura DP.

2.10  Tecniche OR

Sono state utilizzate varie tecniche OR per determinare la soddisfacibilità di un set di clausole. Per esempio, Hooker ha sviluppato un algoritmo cutting plane per risolvere i problemi SAT [61]. Hooker aveva combinato questo con un algoritmo branch­and­bound per ottenere un algoritmo branch­and­cut che mostra qualche promessa [63]. Kamath e al. hanno avuto successo anche con un metodo del punto interno [75].

2.11  Approcci logici

Sono state fatte molte ricerche sulle tecniche SAT da quelli che implementano dimostratori di teoremi del primo ordine. Quanto tempo il SAT è una sottoclasse della logica del primo ordine, alcuni dimostratori di teoremi dovevano contenere inevitabilmente qualche risolutore SAT, anche se si era concentrato poco sulla sua costruzione. Alcuni di questi dimostratori, per esempio la risoluzione basata su Otter [94], ha avuto un rilevante successo e deve essere trattata insieme alla logica proposizionale. Spesso la linea tra proposizionale ed il ragionamento del primo ordine è confusa, per esempio in sistemi che permettono formule quantificate solamente su domini finiti.