En la lógica matemática , un gráfico implicación es un antisimétrica grafo dirigido G = (V, E) compuesta de conjunto de vértices V y dirigida borde conjunto E . Cada vértice en V representa el estado de verdad de un literal booleano , y cada borde dirigido desde el vértice u al vértice v representa la implicación material "Si el literal u es verdadero, entonces el literal v también lo es". Los gráficos de implicación se utilizaron originalmente para analizar expresiones booleanas complejas .
Aplicaciones
Una instancia de 2-satisfacibilidad en forma normal conjuntiva se puede transformar en un gráfico de implicaciones 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 satisfactoria si y solo si ningún literal y su negación pertenecen al mismo componente fuertemente conectado de su grafo de implicación; esta caracterización se puede utilizar para resolver instancias de 2-satisfacibilidad en tiempo lineal. [1]
En los solucionadores CDCL SAT , la propagación de unidades se puede asociar naturalmente con un gráfico de implicaciones que captura todas las formas posibles de derivar todos los literales implícitos de los literales de decisión, [2] que luego se utiliza para el aprendizaje de cláusulas.
Referencias
- ^ Aspvall, Bengt; Plass, Michael F .; Tarjan, Robert E. (1979). "Un algoritmo de tiempo lineal para probar la verdad de ciertas fórmulas booleanas cuantificadas". Cartas de procesamiento de información . 8 (3): 121-123. doi : 10.1016 / 0020-0190 (79) 90002-4 .
- ^ Paul Beame; Henry Kautz; Ashish Sabharwal (2003). Comprender el poder del aprendizaje de cláusulas (PDF) . IJCAI. págs. 1194–1201.