Horn-soddisfacibilita
Horn-soddisfacibilita
Horn-soddisfacibilità particolare connotazione della soddisfacibilità di una formula. In generale una formula si dice soddisfacibile se esiste una interpretazione delle variabili che in essa compaiono, tale che la formula risulti vera (→ soddisfacibilità). Un formula ben formata del linguaggio degli enunciati è una formula di Horn o clausola di Horn se è possibile scriverla come congiunzione di lettere proposizionali (letterali) tutte negative, cioè precedute dal connettivo di negazione indicato dal simbolo ￢, tranne al più una sola che può essere in forma positiva (→ Horn, clausola di). Il problema della Horn-soddisfacibilità (ovvero della soddisfacibilità delle formule di Horn) consiste nel determinare se, dato un insieme di clausole di Horn, è possibile assegnare alle lettere proposizionali dei valori di verità che le rendano tutte vere. Per la risoluzione di tale problema esiste un algoritmo, cioè un procedimento di calcolo, che permette di stabilire, in un numero finito di passi, se un insieme di formule di Horn è soddisfacibile oppure no. L’algoritmo consiste nelle seguenti operazioni:
• si scrivono tutte le formule di Horn come implicazioni;
• si considerano le implicazioni del tipo T ⇒ A (dove T è una qualsiasi tautologia) e si assegna al letterale A il valore di verità V;
• si considerano le implicazioni del tipo
se tutti i letterali A1, A2, …, An hanno valore di verità V (perché è stato loro assegnato al passo precedente) allora si assegna valore di verità V anche al letterale B;
• si considerano le implicazioni del tipo
dove ⊥ è una contraddizione; se tutti i letterali C1, C2, …, Cm hanno valore di verità V (perché assegnato ai passi precedenti) allora l’insieme di formule di Horn considerato non è soddisfacibile; altrimenti – cioè se almeno uno fra i letterali C1, C2, …, Cm non ha valore di verità V – l’insieme di formule di Horn è soddisfacibile con valori di verità V assegnati ai letterali precedentemente considerati e con valori di verità F per tutte le altre.
Come esempio si consideri l’insieme di clausole di Horn:
Per determinare se tale insieme è Horn-soddisfacibile bisogna innanzitutto scrivere ogni clausola come implicazione:
a) A è equivalente a T ⇒ A dove T è una tautologia;
b) B è equivalente a T ⇒ B;
c) ￢A ∨ ￢B ∨ C è equivalente a A ∧ B ⇒ C;
d) ￢A ∨ ￢B ∨ ￢C ∨ D è equivalente a A ∧ B ∧ C ⇒ D;
e) ￢C ∨ ￢E è equivalente a C ∧ E ⇒ ⊥ dove ⊥ è una contraddizione;
Per quanto stabilito al passo b) dell’algoritmo bisogna assegnare il valore V ai letterali A e B. Per il passo c) anche i letterali C e D hanno valore di verità V. Infine per il passo d) si analizza la clausola C ∧ E ⇒ ⊥ in cui il letterale C ha valore di verità V. Si stabilisce quindi che l’insieme delle clausole precedenti è soddisfacibile e che per renderle tutte vere è sufficiente assegnare ai letterali A, B, C, D, E rispettivamente i valori di verità V, V, V, V, F.
In generale, per qualsiasi insieme di enunciati esiste un algoritmo, dato dalle tavole di verità, che permette di stabilire se tale insieme è soddisfacibile oppure no. Ciò che differenzia un insieme di clausole di Horn da un insieme di formule qualsiasi è il fatto che l’algoritmo per stabilire la Horn-soddisfacibilità ha una velocità di convergenza maggiore; è cioè in grado di stabilire se l’insieme di formule è soddisfacibile con un numero minore di operazioni rispetto a quelle che occorre fare per costruire le tavole di verità (→ algoritmo, convergenza di un).