Euristica del simbolo puro

L'euristica del simbolo puro è una euristica utilizzata nel calcolo proposizionale per semplificare l'analisi della soddisfacibilità e la ricerca delle soluzioni di una formula logica. L'euristica del simbolo puro è utilizzata nell'algoritmo DPLL. Un simbolo puro è un letterale che compare nelle clausole sempre nella stessa forma, positiva o negativa. Ad esempio, nella formula il letterale A è un simbolo puro poiché compare sempre nella stessa forma positiva.

( A ∨ B ) ∧ ( A ∨ C ) ∧ ( ¬B ∨ ¬C )

È preferibile analizzare prima i simboli puri, poiché questi possono avere soltanto un valore booleano valido, assegnandogli il valore logico che rende vere le clausole. Ciò consente di ridurre il numero delle clausole della formula e rende più semplice valutare la soddisfacibilità o trovare la soluzione della formula. Ad esempio, nell'esempio precedente è sufficiente assegnare il valore vero al letterale B per ridurre la formula logica alla sola clausola ( ¬B ∨ ¬C ). Analizzando quest'ultima è facile comprendere che la formula è soddisfacibile e ha due soluzioni ( A=vera ∧ B=falsa ), ( A vera ∧ C falsa ), ( A=vera ∧ C=falsa ∧ C=falsa ). In modo analogo nella seguente formula logica il letterale B è un simbolo puro poiché compare sempre nella stessa forma negata (¬B).

( A ∨ ¬B ) ∧ ( ¬A ∨ C ) ∧ ( ¬B ∨ ¬C )

In questo caso è sufficiente assegnare al letterale B il valore falso per rendere vere due clausole e ridurre la formula logica soltanto alla clausola ( ¬A ∨ C ). Analizzando quest'ultima è facile comprendere che la formula è soddisfacibile e ha tre soluzioni ( B=falsa ∧ A=falsa ), ( B falsa ∧ C vera ), ( B falsa ∧ C vera ∧ A=falsa ). La purezza di un simbolo influenza, indirettamente, anche gli altri simboli che inizialmente sono impuri. Ad esempio, nella seguente formula logica il letterale B è un simbolo puro nella sua forma negata ( ¬B ).

Assegnando il valore false al letterale B è possibile rendere vere ed eliminare la prima e la terza clausola. La formula logica si riduce alle due clausole restanti in cui il simbolo C è un nuovo simbolo puro. In altri termini, un letterale impuro può trasformarsi in un simbolo puro durante l'elaborazione ed è importante tenere conto di questo aspetto.

Efficienza. L'euristica del simbolo puro consente di semplificare una formula logica. Ciò permette di verificare più rapidamente la soddisfacibilità logica della formula e la ricerca delle sue soluzioni. L'euristica del simbolo puro è utilizzata in molti algoritmi.