Euristica della clausola unitaria

L'euristica della clausola unitaria è un'euristica del calcolo proposizionale che consente di semplificare l'analisi della soddisfacibilità logica di una formula. Una clausola unitaria è una clausola composta da un unico simbolo letterale ( variabile ). Secondo l'euristica è consigliabile analizzare le clausole unitarie prima delle altre clausole, in quanto ciò consente di effettuare una potatura logica più marcata dell'albero logico. Ad esempio, la seguente formula logica è composta da una clausola unitaria ( ¬C ). Le altre due clausole sono, invece, disgiunzioni di letterali.

In base all'euristica della clausola unitaria il letterale C ( variabile ) dovrebbe essere analizzato prima degli altri due ( A e B ), poiché la soddisfacibilità logica della formula logica è strettamente dipendente dal valore booleano della clausola unitaria ¬C. Selezionando la variabile C, prima delle altre, è facile constatare che qualsiasi soluzione della formula logica deve contemplare l'assegnazione C=false. Dopo aver assegnato il valore di verità ( false ) al letterale C è possibile riscrivere la formula nel seguente modo:

L'assegnazione C=false rende vera la seconda clausola ( ¬C ), consentendo così di eliminarla dalla formula logica, e riduce il numero dei letterali nella terza clausola ( B ∨ C ). Dopo l'applicazione dell'euristica la formula logica si presenta in una forma molto più semplicata: ( A ∨ B ) ∧ ( B ). Oltre a essere più semplifice, la formula logica risultante è composta, a sua volta, da un'altra clausola unitaria ( B ) che emerge dopo aver eliminato il letterale C dalla disgiunzione. È quindi sufficiente analizzare il valore di verità del valore B, in questo caso B=true, per rendere vere le ultime due clausole e, quindi, giungere alla conclusione che la formula logica è soddisfacibile.

Nell'esempio precedente l'euristica della clausola unitaria ha analizzato la soddisfacibilità della formula logica e restituito una soluzione valida al problema ( C=false ∧ B=true ) in soli due operazioni. Per giungere alla medesima conclusione ( soddisfacibilità della formula ) l'algoritmo DPLL avrebbe impiegato sei passaggi. Nella seguente rappresentazione è possibile seguire tutte le operazioni di assegnazione svolte dall'algoritmo DPLL prima di giungere alla prima soluzione valida.

Algoritmo DPLL / DP. L'euristica della clausola unitaria non è un vero e proprio metodo di verifica di soddisfacibilità logica in quanto non sempre consente di risolvere un problema di soddisfacibilità. Ad esempio nel seguente esempio l'euristica si limita a semplificare la formula logica senza giungere a una conclusione sulla soddisfacibilità della stessa. La formula semplificata ( A ∨ B ) non permette di affermare o meno la soddisfacibilità della formula logica senza svolgere ulteriori calcoli.

In conclusione, l'euristica della clausola unitaria consente soltanto di semplificare la formula logica, di effettuare una potatura logica efficace sull'albero di ricerca e di migliorare l'efficienza degli algoritmi specifici nella verifica della soddisfacibilità come, ad esempio, l'algoritmo DP o l'algoritmo DPLL.