title: Grafo delle implicazioni
text: # Grafo delle implicazioni
  
  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.
  
  