Gráfico de implicación

En lógica matemática y teoría de grafos , un grafo de implicación es un grafo dirigido y antisimétrico G = ( V , E ) compuesto por un conjunto de vértices V y un conjunto de aristas dirigidas E. Cada vértice en V representa el estado de verdad de un literal booleano , y cada arista dirigida desde el vértice u hasta el vértice v representa la implicación material "Si el literal u es verdadero, entonces el literal v también es verdadero". Los grafos de implicación se utilizaron originalmente para analizar expresiones booleanas complejas .

Una instancia de 2-satisfacibilidad en forma normal conjuntiva se puede transformar en un gráfico de implicación reemplazando cada una de sus disyunciones por un par de implicaciones. Por ejemplo, la declaración se puede reescribir como el par . Una instancia es satisfacible si y solo si ningún literal y su negación pertenecen al mismo componente fuertemente conectado de su gráfico de implicación; esta caracterización se puede utilizar para resolver instancias de 2-satisfacibilidad en tiempo lineal . ^[1]${\displaystyle (x_{0}\lor x_{1})}$${\displaystyle (\neg x_{0}\rightarrow x_{1}),(\neg x_{1}\rightarrow x_{0})}$

En los solucionadores SAT de CDCL , la propagación de unidades se puede asociar naturalmente con un gráfico de implicación que captura todas las formas posibles de derivar todos los literales implícitos a partir de literales de decisión, ^[2] que luego se utiliza para el aprendizaje de cláusulas.