Il metodo di risoluzione

La lezione sulla semantica della logica proposizionale ha mostrato che la validità e la soddisfacibilità sono decidibili con la tavola di verità, a un costo che raddoppia a ogni variabile, e ha annunciato metodi che non richiedessero di percorrerla. La lezione su conseguenza ed equivalenza semantica ha ridotto ogni conseguenza a un’insoddisfacibilità: $\Gamma \models \varphi$ se e solo se $\Gamma \cup \{\neg\varphi\}$ è insoddisfacibile. Le lezioni sulle forme normali e sul loro algoritmo hanno dato a ogni formula una forma congiuntiva, la cui validità si vede a colpo d’occhio, ma la cui soddisfacibilità non si vede. Se le cose stanno così, manca una procedura che decida l’insoddisfacibilità di una congiunzione di clausole operando sulle clausole stesse. Questa procedura è la risoluzione, proposta da John Alan Robinson nel 1965 su idee di Martin Davis e Hilary Putnam (1960); è il nucleo dei programmi che oggi decidono la soddisfacibilità di formule con milioni di variabili. A differenza del sistema dell’unità sulla deduzione, le cui relazioni con la semantica sono studiate dalle lezioni sulla correttezza e completezza e su il teorema di compattezza, la risoluzione non deduce conclusioni: refuta insiemi. Questa lezione dimostra che lo fa in modo corretto e completo.

Come nelle lezioni precedenti, $p$, $q$, $r$, $s$ e $t$ indicano le variabili da $v_1$ a $v_5$; la lettera $v$ senza indice, e anche $w$, designano assegnazioni; e $V(\varphi)$ è l’insieme delle variabili di $\varphi$.

Clausole e insiemi di clausole

Si ricordi dalla lezione sulle forme normali che un letterale è una variabile o la negazione di una variabile, e che l’opposto di un letterale $\ell$, scritto $\ell^{*}$, è il letterale della stessa variabile e dell’altro segno; due letterali opposti formano una coppia complementare. Per il lemma sulla negazione di un letterale, $v(\ell^{*}) = 1 - v(\ell)$ per ogni assegnazione $v$. Là una clausola era una disgiunzione di letterali; qui conviene dimenticare l’ordine e le ripetizioni, che non alterano il valore, e tenersi l’insieme.

Una clausola è un insieme finito di letterali. La clausola senza letterali si chiama clausola vuota e si scrive $\Box$. Un’assegnazione $v$ soddisfa una clausola $C$, e si scrive $v \models C$, se qualche letterale di $C$ vale $1$ in $v$; in caso contrario, $v$ la refuta. Una clausola di un solo letterale si chiama unitaria. Le variabili di una clausola formano l’insieme $V(C)$; quelle di un insieme $S$ di clausole, l’insieme $V(S)$, unione dei precedenti. Un’assegnazione soddisfa un insieme $S$ di clausole, $v \models S$, se soddisfa ciascuna delle sue clausole; $S$ è soddisfacibile se qualche assegnazione lo soddisfa, e insoddisfacibile in caso contrario. Infine, se $S$ è un insieme di clausole e $C$ una clausola, $S \models C$ significa che ogni assegnazione che soddisfa $S$ soddisfa $C$.

Due casi estremi seguono dalla definizione, e conviene fissarli. La clausola vuota non ha letterali; quindi nessun suo letterale vale $1$, e nessuna assegnazione la soddisfa: $\Box$ è insoddisfacibile, e lo è anche ogni insieme che la contenga. L’insieme vuoto di clausole, invece, non ha clausole da soddisfare, e ogni assegnazione lo soddisfa. Non vanno confusi: $\{\Box\}$ è insoddisfacibile e $\emptyset$ è soddisfatto da tutte le assegnazioni.

Una clausola che contiene una coppia complementare si chiama tautologica: non impone alcuna condizione e può essere tolta da qualsiasi insieme senza alterarne i modelli. Scrivere le clausole come insiemi non è un capriccio di notazione. Se da $(p \vee q)$ e $(p \vee \neg q)$ si vuole ottenere $p$, la disgiunzione dà $(p \vee p)$, che equivale a $p$ ma non è la stessa formula; con gli insiemi, $\{p\} \cup \{p\} = \{p\}$, e la fusione dei letterali ripetuti avviene da sola.