Una stessa formula logica si può scrivere in infiniti modi equivalenti. Per confrontare formule, semplificarle o darle in pasto a un programma conviene ridurle a una forma standard. Le due forme standard più usate sono la forma normale disgiuntiva (DNF) e la forma normale congiuntiva (CNF). Capirle significa capire anche come lavorano gli strumenti di verifica automatica e i progettisti di circuiti.
I mattoni: letterali e clausole
- Un letterale è una variabile o la sua negazione: p, ¬p, q, ¬q.
- Una congiunzione di letterali è un AND di letterali, per esempio p ∧ ¬q ∧ r.
- Una clausola è un OR di letterali, per esempio ¬p ∨ q ∨ ¬r.
Con questi mattoni:
- la DNF è un OR di congiunzioni di letterali: (p ∧ ¬q) ∨ (¬p ∧ r) ∨ q;
- la CNF è un AND di clausole: (p ∨ q) ∧ (¬p ∨ r) ∧ (¬q ∨ ¬r).
Un modo per ricordarle: la DNF descrive i casi in cui la formula è vera («è vera se succede questo, oppure questo, oppure questo»); la CNF elenca vincoli che devono valere tutti insieme («deve valere questo, e questo, e questo»).
Ricavare la DNF da una tavola di verità
Il metodo è meccanico. Per ogni riga in cui la formula vale V si scrive una congiunzione che descrive esattamente quella riga: la variabile così com'è se vale V, negata se vale F. Poi si uniscono tutte con OR.
Prendiamo la formula «esattamente una tra p e q è vera» (lo XOR):
| p | q | p ⊕ q |
|---|---|---|
| V | V | F |
| V | F | V |
| F | V | V |
| F | F | F |
Le righe vere sono la seconda (p vero, q falso) e la terza (p falso, q vero). La DNF è quindi (p ∧ ¬q) ∨ (¬p ∧ q).
Ricavare la CNF da una tavola di verità
Il metodo è il duale. Per ogni riga in cui la formula vale F si scrive una clausola che è falsa solo in quella riga: la variabile negata se vale V, così com'è se vale F. Poi si uniscono le clausole con AND.
Per lo XOR le righe false sono la prima (p e q veri) e la quarta (entrambi falsi). La prima dà la clausola ¬p ∨ ¬q, la quarta p ∨ q. La CNF è (p ∨ q) ∧ (¬p ∨ ¬q). Si legge bene: «almeno una è vera, e non sono vere entrambe».
Trasformazione algebrica
Quando la tavola è troppo grande si procede con le equivalenze:
- Eliminare ↔ e →, usando p → q ≡ ¬p ∨ q.
- Portare le negazioni sui letterali con De Morgan e la doppia negazione.
- Applicare la distributività: per la CNF si distribuisce ∨ su ∧; per la DNF ∧ su ∨.
Esempio: trasformare in CNF la formula p ∨ (q ∧ r). Distribuendo si ottiene (p ∨ q) ∧ (p ∨ r).
C'è un problema pratico: la distributività può far crescere la formula in modo esponenziale. La formula (a₁ ∧ b₁) ∨ (a₂ ∧ b₂) ∨ … ∨ (aₙ ∧ bₙ) ha una CNF equivalente con 2ⁿ clausole. Per questo gli strumenti reali usano la trasformazione di Tseitin, che introduce variabili ausiliarie e produce una CNF di dimensione lineare. La formula ottenuta non è equivalente in senso stretto, ma è equisoddisfacibile: è soddisfacibile se e solo se lo è l'originale, e per molti scopi basta.
Perché la CNF è così importante
Il problema SAT chiede se una formula ammette almeno un'assegnazione che la rende vera. I programmi che lo risolvono, i SAT solver, accettano quasi sempre l'input in CNF, spesso nel formato testuale chiamato DIMACS:
p cnf 3 2
1 -2 0
2 3 0
La riga di intestazione dice che ci sono 3 variabili e 2 clausole; ogni riga successiva è una clausola, con i numeri negativi per i letterali negati e lo zero come terminatore. Questo esempio rappresenta (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃).
La CNF si presta bene alla ricerca automatica perché ogni clausola è un vincolo indipendente: se un'assegnazione parziale rende falsi tutti i letterali di una clausola tranne uno, quell'ultimo letterale è obbligato. Questa regola, chiamata propagazione unitaria, è il cuore degli algoritmi DPLL e CDCL. I SAT solver vengono usati per verificare hardware, pianificare, risolvere puzzle combinatori e analizzare le dipendenze tra pacchetti software.
E la DNF?
La DNF rende banale la domanda opposta: una formula in DNF è soddisfacibile se almeno una delle sue congiunzioni non contiene una variabile insieme alla sua negazione. Il prezzo è che verificare se una DNF è una tautologia diventa difficile. Nella progettazione di circuiti la DNF corrisponde alla struttura «somma di prodotti», realizzabile con un livello di porte AND seguito da una porta OR, e si minimizza con le mappe di Karnaugh o con l'algoritmo di Quine-McCluskey.
In sintesi
- La DNF è un OR di AND di letterali; la CNF è un AND di OR di letterali, cioè di clausole.
- Dalla tavola di verità: righe vere per la DNF, righe false per la CNF.
- La trasformazione algebrica può esplodere esponenzialmente; Tseitin produce una CNF equisoddisfacibile di dimensione lineare.
- I SAT solver lavorano in CNF, tipicamente nel formato DIMACS.
- La DNF corrisponde ai circuiti «somma di prodotti».
