저녁밥

저녁밥

Front-end Developer

5장 알고리즘의 정당성 증명

Updated:
5 minute read

5.1 도입

본 글에서는 알고리즘의 증명을 위해 흔히 사용하는 기법들을 간략하게 다른다.

여기서 다루는 증명 방식은 비구성적 증명(nonconstructive proof)로서 ‘어떤 답이 존재한다’고 증명하는 것이 아닌, 답의 존재 유무 만을 증명한다.

5.2 수학적 귀납법과 반복문 불변식

수학적 귀납법(Mathmetical Induction)의 증명은 크게 세 단계로 나뉜다.

  1. 단계 나누기: 증명하고 싶은 사실을 여러 단계로 나눈다.
  2. 첫 단계 증명: 여러 단계 중 첫 단계에서 증명하고 싶은 내용이 성립함을 보인다.
  3. 귀납 증명: 한 단계에서 증명하고 싶은 내용이 성립한다면, 다음 단계에서도 성립함을 보입니다.

반복문 불변식

반복문 불변식(Loop Invariant)
반복문이 한 번씩 실행될 때마다 제대로 작동하고 있는지 판단할 수 있는 참거짓의 형태의 논리적 단정문(logical assertion)

불변식을 이용하여 반복문의 정당성을 다음과 같이 증명할 수 있다.

  1. 반복문 진입시에 불변식이 성립함을 보인다.
  2. 반복문 내용이 불변식을 깨뜨리지 않음을 보인다. (반복문이 한 번 수행하고 나서도 불변식이 항상 성립함을 보인다.)
  3. 반복문 종료시에 불변식이 성립하면 항상 우리가 정답을 구했음을 보인다.

삽입 정렬과 반복문 불변식

void insertionSort(vector<int>& A) {
    for(int i = 0; i < A.size(); ++i) {
        // 불변식 a: A[0..i - 1]은 이미 정렬되어 있다.
        // A[0..i - 1]에 A[i]를 끼워넣는다.
        int j = i;
        while(j > 0 && A[j-1] > A[j]) {
        // 불변식 b: A[j + 1..i]의 모든 원소는 A[j]보다 크다.
        // 불변식 c: A[0..i]구간은 A[j]를 제외하면 정렬되어 있다.
        swap(A[j-1], A[j]);
        --j;
        }
    }
}

for문의 정당성

(a) 초기조건 반복문이 시작할 때 i = 0이면 해당 구간은 비어 있으니 항상 정렬되어 있다고 가정할 수 있다.

(a) 불변식 유지 for문의 내용이 종료할 때 이 불변식이 깨지지 않고 유지됨을 보이기 위해서는 while문의 정당성을 증명해야 한다.

while문의 정당성

(b) 초기조건 while문 진입시에 A[j + 1..i]구간은 빈 구간이므로 (b)는 참이다.

(b) 불변식 유지 while문 내용이 실행되었다는 말은 A[j-1] > A[j]라는 의미이니, swap(A[j-1], A[j])하고 --j하면 (b)는 여전히 참이다.

(c) 초기조건 불변식 (a)에 의해 구간 A[0..i - 1]은 정렬되어 있으니 while문 진입시에 (c)는 참이다.

(c) 불변식 유지 swap(A[j-1], A[j])을 해도 A[j] 앞에 있는 원소들의 상대적 순서와 뒤에 있는 원소들의 상대적 순서는 변하지 않기 때문에 (c) 또한 항상 참이다.

5.3 귀류법

귀류법
원하는 바와 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내는 증명 기법

상자 쌓기

책에선 책장 쌓기로 소개하지만 본 글에선 문제를 단순화하기 위해 상자 쌓기로 소개합니다.

상자를 여러 개 쌓아올릴려고 한다. 각 상자마다 버틸 수 있는 최대 무게 Mi와 자신의 무게 Wi가 주어질 때 상자를 가장 높이 쌓는 방법은 무엇인가?

  • 정답 Mi + Wi 가 큰 것부터 아래에 놓아야 한다.

이를 증명하기 위해 정답의 반대를 가정한다.

  • MA + WA > MB + WB인 상자 A가 B 위에 있다.

또한 A위에 올라가 있는 상자들의 무게의 합을 X라고 하다면 다음이 성립힌다.

  • MB >= WA + X

여기서 상자 A와 B의 위치가 뒤바뀌어도 여전히 최적해라는 것을 보여서 정답을 증명한다.

  • MA + WA > MB + WB
  • MA > MB + WB - WA
  • MA > MB + WB - WA >= (WA + X ) + WB - WA
  • MA > (WA + X ) + WB - WA

상자 A는 상자 B의 무게와 그 위의 모든 상자를 지탱할 수 있으므로 A와 B의 위치를 바꿔도 된다.

따라서, Mi + Wi 가 큰 것부터 아래에 놓았을 때 최적해를 얻지 못하는 경우는 존재하지 않는다.

5.4 다른 기술들

비둘기집 원리

비둘기집 원리
n+1개의 물건을 n개의 상자에 넣을 때 적어도 어느 한 상자에는 두 개 이상의 물건이 들어 있다는 원리

순환 소수 찾기

// 분수 a/b의 소수 표현을 출력한다.
// a >= 0, b > 0 이라고 가정함
void printDecimal(int a, int b) {
    int iter = 0;
    while(a > 0) {
        // 첫 번째와 두 번째 사이에 소수점을 찍는다.
        if(iter++ == 1) cout << '.';
        cout << a / b;
        a = (a % b) * 10;
    }
}

위 코드에서 무한 소수를 인식하기 위해선 어떻게 해야 할까

비둘기 집의 원리를 활용한다.

a % b의 결과는 언제나 [0, b-1]의 범위의 값을 갖는다. 즉 a % b는 b가지의 결과만 가질 수 있는 것이다.

그래서 while문이 b+1번 반복될 때까지 함수가 종료하지 않으면 a = (a % b) * 10의 값이 중복되는 결과가 반드시 존재하므로 순환 소수임을 알 수 있다.

구성적 증명

비구성적 증명이 답의 존재 유무를 증명하는 것이라면, 구성적 증명(constructive proof)은 특정 답을 통해 알고리즘의 정당성을 입증하는 접근법이다.

안정적 결혼 문제는 구성적 증명의 대표적인 문제이다.

안정적 결혼 문제

n명의 남성과 n명의 여성이 있으며 모두는 이성에 대해서 1등부터 n등까지 선호하는 각자의 순위가 있다.(공동 순위는 없다.) 현재의 상대방보다 선호하는 이성도 자신을 더 선호하는 경우가 없도록 짝을 짓는 방법이 존재하는가?

이 문제는 답의 존재성을 보이는 대신 답을 만드는 알고리즘을 제시함으로써 답이 존재함을 보였다.

알고리즘은 다음과 같다.

  1. 남성들은 자신이 가장 선호하는 여성에게 프로포즈를 하고 여성은 자신에게 프로포즈를 한 남성들 중 가장 선호하는 남성과 짝이 된다.
  2. 짝이 없는 남성들은 다음으로 선호하는 여성에게 프로포즈를 한다.
    • 짝이 없는 여성은 프로포즈 한 남성들 중 가장 선호하는 남성과 짝이 된다.
    • 짝이 있는 여성이 자신의 짝보다 더 선호하는 남성에게 프로포즈를 받는다면 그 사람과 짝이되고 그렇지 않다면 프로포즈를 거절한다.
  3. 더 프로포즈할 남성이 없을 때까지 반복한다.

이 알고리즘이 문제를 제대로 해결할 수 있는지 확인하기 위해 알고리즘이 항상 종료하는지, 또 그 결과가 항상 안정적인지 증명해야 한다.

종료 증명

각 남성은 거절당할 때마다 다음 우선순위의 여성에게 프로포즈하기 때문에 최대 N명의 여성에게 순서대로 프로포즈 한 뒤에는 이 과정이 반드시 종료된다.

모든 사람들이 짝을 찾는지 증명

아무리 짝을 못구하는 남성이라도 모든 여성에게 한 번씩은 프로포즈를 하며 한 번이라도 프로포즈를 받은 여성은 반드시 짝이 있기 때문에 짝을 찾지 못한 사람은 있을 수 없다.

Back to top ↑

Leave a comment

You may also enjoy