Scomposizione clausole
La scomposizione delle clausole è un'euristica utilizzata nel calcolo proposizionale per semplificare lo studio della soddisfacibilità logica di una formula logica. Ogni clausola viene scomposta in sottoinsiemi di disgiunzioni logiche ( detti componenti ), in uno dei quali sono raggruppati i letterali non in comune con le altre clausole. Se una clausola comprende un letterale specifico ( non in comune ), è sufficiente trovare il suo valore di verità per rendere vera l'intera clausola ed eliminarla dalla formula logica. Ad esempio, nella seguente formula logica la terza clausola è caratterizzata dal letterale non in comune (C). Assegnando il valore booleano vero ( true ) al letterale C è possibile semplificare la formula logica in ( A ∨ B ) ∧ ( ¬B ∨ C ).
L'assegnazione del valore booleano "true" ( vero ) al letterale D consente di effettuare una potatura logica dell'albero di ricerca senza influire sulle restanti clausole. In conclusione, la scomposizione della formula logica semplifica la formula logica da analizzare. Ciò è particolarmente utile prima di eseguire un algoritmo di analisi della soddisfacibilità di un problema CNF in quanto riduce il numero delle operazioni necessarie per verificare l'esistenza di almeno una soluzione del problema.
Efficienza. L'analisi della soddisfacibilità dei singoli componenti di una formula logica riduce la complessità del calcolo proposizionale e le operazioni necessarie per comprendere se la formula è soddisfacibile logicamente o meno, ossia se ha almeno una soluzione ( soddisfacibile ) o non ha soluzioni ( insoddisfacibile ).
Algoritmo DPLL. L'euristica della scomposizione delle clausole è utilizzata ricorsivamente, ad esempio, nell'algoritmo DPLL per semplificare una formula logica prima di procedere all'assegnazione dei valori booleani ai singoli letterali delle clausole. Durante l'elaborazione la formula logica si trasforma continuamente, è quindi opportuno eseguire l'euristica della scomposizione delle clausole ogni volta che la formula logica viene modificata.
