인증 알고리즘

Certifying algorithm

이론 컴퓨터 공학에서, 증명 알고리즘은 해결한 문제에 대한 해결책과 함께 솔루션이 옳다는 증거를 출력하는 알고리즘입니다.증명 알고리즘은 알고리즘과 프루프 체커의 조합된 실행시간이 같은 [1]문제에 대해 가장 잘 알려진 비증명 알고리즘보다 최대 일정한 계수만큼 느릴 경우 효율적이라고 할 수 있다.

증명 알고리즘에 의해 생성되는 증명은 어떤 의미에서는 알고리즘 자체보다 단순해야 합니다.그렇지 않으면 어떤 알고리즘도 증명된 것으로 간주될 수 있습니다(같은 알고리즘을 다시 실행하여 출력을 검증).경우에 따라서는, 증명 검증에 원래의 알고리즘보다 시간이 적게 걸리는 것으로써, 그 외의 문제(특히 선형 시간내에 솔루션을 찾을 수 있는 문제)에 대해서는, 출력 증명의 심플함을 덜 형식적인 [1]의미로 생각할 수 있습니다.예를 들어 출력증명의 유효성이 알고리즘의 정확성보다 인간 사용자에게 더 명확할 수도 있고, 또는 증명용 체커가 공식 [1][2]검증에 더 적합할 수도 있다.

알고리즘에 의해 생성된 증명에 대한 체커를 포함한 증명 알고리즘의 실장은 비인증 알고리즘보다 신뢰성이 높은 것으로 간주될 수 있다.알고리즘이 실행될 때마다 다음 세 가지 중 하나가 발생합니다.올바른 출력(필요한 경우), 알고리즘 내의 버그 또는 그 영향(필요하지는 않지만 일반적으로 버그를 검출하지 않고 계속하는 것보다 바람직함), 또는 알고리즘과 체커가 모두 오류를 은폐하고 오류를 방지하는 방식으로 장애가 발생합니다.검출되었습니다(필요하지만, 2개의 독립된 [1]버그의 존재에 의존하기 때문에 가능성이 낮습니다).

예

체크 가능한 알고리즘에 관한 문제의 많은 예는 그래프 이론에서 비롯된다.예를 들어, 그래프가 초당인지 여부를 테스트하는 고전적인 알고리즘은 단순히 부울 값을 출력합니다. 그래프가 초당이면 true이고 그렇지 않으면 false입니다.이와는 대조적으로 증명 알고리즘은 초당인 경우 그래프의 2색 또는 홀수 길이의 사이클을 출력할 수 있습니다.그래프는 2색일 수 있는 경우에만 쌍방향이며, 홀수 주기를 포함하는 경우에만 쌍방향입니다.2색상이 유효한지 여부를 확인하는 것과 주어진 홀수 길이의 정점 시퀀스가 사이클인지 확인하는 것은 모두 초당성을 [1]테스트하는 것보다 더 단순하게 수행될 수 있습니다.

마찬가지로 토폴로지 순서 또는 방향 사이클 중 하나를 출력하는 증명 알고리즘에 의해 주어진 방향 그래프가 비순환인지 여부를 테스트할 수 있다.무방향 그래프가 코드 그래프인지 아닌지를 증명하는 알고리즘에 의해 테스트할 수 있습니다.증명 알고리즘은 제거 순서(모든 정점에 대해 순서 뒤에 있는 인접 라우터가 클리크를 형성하도록 모든 정점의 순서)를 출력합니다.그리고 평면 매립 또는 Kuratowski 서브그래프를 [1]출력하는 인증 알고리즘에 의해 그래프가 평면인지 테스트할 수 있다.

두 정수 x와 y의 최대공약수에 대한 확장 유클리드 알고리즘은 이를 증명한다: 그것은 세 정수 g(제수), a, b를 출력한다. 즉, ax + b는 = g이다.이 방정식은 최대공약수의 배수에만 해당되므로 g가 최대공약수이고 g가 x와 y를 나눈다는 것과 이 방정식이 올바른지 [1]확인함으로써 g가 최대공약수라는 것을 테스트할 수 있습니다.

「 」를 참조해 주세요.

  • 건전성 검사: 출력 또는 중간 결과의 정확성에 대한 간단한 테스트로, 정확성의 완전한 증거가 될 필요는 없습니다.

레퍼런스

  1. ^ a b c d e f g 를 클릭합니다McConnell, R.M.; Mehlhorn, K.; Näher, S.; Schweitzer, P. (May 2011), "Certifying algorithms", Computer Science Review, 5 (2): 119–161, doi:10.1016/j.cosrev.2010.09.009.
  2. ^ 를 클릭합니다Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine (June 2013), "A Framework for the Verification of Certifying Computations", Journal of Automated Reasoning, 52 (3): 241–273, arXiv:1301.7462, doi:10.1007/s10817-013-9289-2.