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 si possono dedurre logicamente le espressioni e , per poi rappresentarle nel grafo. Le altre implicazioni si deducono in maniera analoga.