알고리즘의 정당성 증명

지식 저장소·2021년 11월 24일
0

문제해결기법

목록 보기
5/21

수학적 귀납법

수학적 귀납법은 반복적인 구조를 갖는 명제들을 증명하는 데 유용하게 사용되는 증명 기법입니다. 귀납법 증명은 크게 세 단계로 나누어집니다.

  • 단계 나누기: 증명하고 싶은 사실을 여러 단계로 나눕니다.
  • 첫 단계 증명: 첫 단계에서 증명하고 싶은 내용이 성립합을 보입니다.
  • 귀납 증명: 어떤 한 단계에서 증명하고 싶은 내용이 성립한다면, 다음 단계에서도 성립하는지 보입니다.

반복문 불변식

귀납법을 이용해 알고리즘의 정당성을 증명할 때는 반복문 불변식이라는 개념이 유용하게 쓰입니다. 반복문 불변식이란 반복문의 내용이 한 번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건입니다.
불변식을 이용하면 반복문의 정당성을 다음과 같이 증명할 수 있습니다.

  1. 반복문 진입시에 불변식이 성립함을 보인다.
  2. 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. 다르게 말하면, 반복문 내용이 시작할 때 불변식이 성립했다면 내용이 끝날 때도 불변식이 항상 성립함을 보인다.
  3. 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.

이진 탐색과 반복문 불변식

// 필수 조건: A는 오름차순으로 정렬되어 있다.
// 결과: A[i - 1] < x <= A[i]인 i를 반환한다.
// 이때 A[-1] = 음의 무한대, A[n] = 양의 무한대라고 가정한다.
int binsearch(const vector<int>& A, int x) {
	int n = A.size();
    int lo = -1, hi = n;
    // 반복문 불변식 1: lo < hi
    // 반복문 불변식 2: A[lo] < x <= A[hi]
    // (*) 불변식은 여기서 성립해야 한다.
    while(lo + 1 < hi) {
    	int mid = (lo + hi) / 2;
        if(A[mid] < x)
        	lo = mid;
        else
        	hi = mid;
        // (**) 불변식은 여기서도 성립해야 한다.
    }
  	return hi;
}

이 코드가 실행될 때 반복문 불변식인 lo < hi와 A[lo] < x <= A[hi]를 만족하는지 확인해야 합니다. 까다로운 코드를 짤 때 해당 코드가 가져야 할 불변식을 파악하고 작성하면 좀더 오류가 적은 코드를 작성할 수 있습니다.

귀류법

귀류법이란 증명해야할 명제와 반대되는 명제를 참이라고 가정하고 논리를 전개해서 모순을 찾아서 증명하는 기법을 귀류법이라고 합니다. 귀류법은 대게 어떤 선택이 항상 최선임을 증명하고자 할 때 많이 이용됩니다. 우리가 선택한 답보다 좋은 답이 있다고 가정한 후에, 사실은 그런 일이 있을 수 없음을 보이면 우리가 최선의 답을 선택했음을 보일 수 있기 때문입니다.

다른 기술들

비둘기집의 원리

101마리의 비둘기가 100개의 비둘기집에 모두 들어갔다면, 2마리 이상이 들어간 비둘기집이 반드시 하나는 있게 마련이다.

위 글만 보고도 알 수 있을만큼 쉬운 이론입니다.

구성적 증명

구성적 증명이란 답의 실제 예를 들거나 답을 만드는 방법을 실제로 제시하는 증명입니다. 이 증명은 우리가 원하는 어떤 답이 존재한다는 사실을 증명하기 위해서 사용됩니다.

참고문헌: 구종만, 프로그래밍 대회에서 배우는 알고리즘 문제해결전략, 인사이트, (2012)

profile
그리디하게 살자.

0개의 댓글