Grafo delle implicazioni

Grafo delle implicazioni rappresentante l'istanza del problema 2-satisfiability rappresentata dall'espressione:$\scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptscriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).$

In logica matematica, un grafo delle implicazioni è un grafo orientato G(V, E) composto da un insieme di vertici V ed un insieme di archi E. Ogni vertice in V rappresenta l'assegnazione booleana di un letterale, ed ogni arco orientato da un vertice u ad un vertice v rappresenta l'implicazione materiale "Se il letterale u è vero allora lo è anche illetterale v". Viene utilizzato per analizzare le espressioni booleane più complesse.

Applicazioni

Un'istanza di 2-satisfiability in forma normale congiuntiva può essere rappresentata da un grafo delle implicazioni sostituendo ognuna delle sue clausole da una coppia di implicazioni. Un'istanza di 2-SAT è soddisfacibile se e solo se nessun letterale e la sua negazione derivano dalla stessa componente fortemente connessa del grafo associato; questo metodo è utilizzato per risolvere il problema di soddisfacibilità con clausole binarie in tempo polinomiale.

Nell'esempio fornito sulla destra, dalla clausola $x_{0}\lor \lnot x_{3}$ si possono dedurre logicamente le espressioni $x_{3}\to x_{0}$ e $\lnot x_{0}\to \lnot x_{3}$, per poi rappresentarle nel grafo. Le altre implicazioni si deducono in maniera analoga.