Algoritmo de certificación

En informática teórica , un algoritmo certificador es aquel que produce, junto con la solución al problema que resuelve, una prueba de que dicha solución es correcta. Se dice que un algoritmo certificador es eficiente si el tiempo de ejecución combinado del algoritmo y un verificador de pruebas es, como máximo, más lento por un factor constante que el mejor algoritmo no certificador conocido para el mismo problema. ^{[ 1 ]}

La prueba producida por un algoritmo certificador debería ser, en cierto sentido, más simple que el algoritmo mismo, ya que de lo contrario cualquier algoritmo podría considerarse certificador (y su resultado se verificaría ejecutando el mismo algoritmo nuevamente). A veces, esto se formaliza exigiendo que la verificación de la prueba tome menos tiempo que el algoritmo original, mientras que para otros problemas (en particular aquellos cuya solución se puede encontrar en tiempo lineal ) la simplicidad de la prueba resultante se considera en un sentido menos formal. ^{[ 1 ]} Por ejemplo, la validez de la prueba resultante puede ser más evidente para los usuarios humanos que la corrección del algoritmo, o un verificador de la prueba puede ser más susceptible a la verificación formal . ^{[ 1 ] [ 2 ]}

Las implementaciones de algoritmos de certificación que también incluyen un verificador para la prueba generada por el algoritmo pueden considerarse más fiables que los algoritmos sin certificación. Porque, cada vez que se ejecuta el algoritmo, sucede una de tres cosas: produce una salida correcta (el caso deseado), detecta un error en el algoritmo o en sus implicaciones (no deseado, pero generalmente preferible a continuar sin detectar el error), o tanto el algoritmo como el verificador son defectuosos de tal manera que enmascaran el error e impiden su detección (no deseado, pero improbable, ya que depende de la existencia de dos errores independientes). ^{[ 1 ]}

Muchos ejemplos de problemas con algoritmos verificables provienen de la teoría de grafos . Por ejemplo, un algoritmo clásico para comprobar si un grafo es bipartito simplemente arrojaría un valor booleano: verdadero si el grafo es bipartito, falso en caso contrario. En cambio, un algoritmo certificador podría arrojar una coloración de dos colores del grafo en caso de que sea bipartito, o un ciclo de longitud impar si no lo es. Cualquier grafo es bipartito si y solo si se puede colorear con dos colores, y no bipartito si y solo si contiene un ciclo impar. Tanto comprobar si una coloración de dos colores es válida como comprobar si una secuencia de vértices de longitud impar dada es un ciclo pueden realizarse de forma más sencilla que comprobar la bipartición. ^{[ 1 ]}

De forma análoga, es posible comprobar si un grafo dirigido dado es acíclico mediante un algoritmo de certificación que produce un orden topológico o un ciclo dirigido. Es posible comprobar si un grafo no dirigido es un grafo cordal mediante un algoritmo de certificación que produce un ordenamiento de eliminación (un ordenamiento de todos los vértices tal que, para cada vértice, los vecinos que aparecen más tarde en el ordenamiento forman una camarilla ) o un ciclo sin cuerdas. Y es posible comprobar si un grafo es planar mediante un algoritmo de certificación que produce una incrustación planar o un subgrafo de Kuratowski . ^{[ 1 ]}

El algoritmo euclidiano extendido para el máximo común divisor de dos enteros x e y es certificante: produce tres enteros g (el divisor), a y b , tales que ax + by = g . Esta ecuación solo puede ser verdadera para múltiplos del máximo común divisor, por lo que se puede comprobar que g es el máximo común divisor verificando que g divide tanto a x como a y y que esta ecuación es correcta. ^{[ 1 ]}

• Verificación de cordura , una prueba simple de la corrección de una salida o resultado intermedio que no requiere ser una prueba completa de corrección.