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.

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.^[1]

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

Portale Matematica: accedi alle voci di Teknopedia che trattano di matematica