알고리즘의 정당성 증명

dlwogns·2023년 12월 31일

algorithm

목록 보기

2/6

출처 : 종만북

수학적 귀납법

반복적인 구조를 같는 명제들을 증명하는데 유용하게 사용되는 증명기법.

수학적 귀납법의 구조

단계 나누기
증명하고 싶은 사실을 여러 단계로 나눈다. 100개의 도미노를 도미노 하나씩으로 나누는 과정을 의미한다.
첫 단계 증명(basic step)
첫 단계에서 증명하고 싶은 내용이 성립함을 보임. 첫번째 도미노가 넘어짐을 증명하는 과정을 의미한다.
귀납 증명(inductive step)
한 단계에서 증명하고 싶은 내용이 성립한다면, 다음 단계에서도 성립함을 보임. 한 도미노가 쓰러지면 다음 도미노는 반드시 쓰러짐을 보이는 과정을 의미한다.

반복문 불변식

반복적인 요소를 가지고 있는 알고리즘에서 귀납법을 통해 알고리즘의 반복적인 각 단계가 정답으로 가는 길 위에 있음을 보이고, 알고리즘의 답이 옳음을 보인다.
이때 반복 과정에서 반복 내용이 한번 실행될 때마다 중간 결과가 우리가 원하는 답으로 가는 길 위에 잘 있는지를 명시하는 조건을 반복문 조건식(loop-invariant)이라 한다.

불변식을 이용한 반복문의 정당성

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

예시 : 이진 탐색

// 필수 조건: 배열 A는 오름차순으로 정렬되어 있다.
// 결과 : A[i-1] < x <= A[i]인 i를 반환한다.
	
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) // invariant 2 : x <= A[hi]이기 때문에 반대조건시 lo에 mid 할당.
    	lo = mid;
    else
    	hi = mid;
	// 반복문 내용이 끝나는 이시점, 불변식이 성립해야 한다.
}
// hi -> 정답

lo + 1 = hi (중요)
while이 종료했으니 lo + 1 >= hi라는 것을 알 수 있다. lo < hi를 불변식으로 항상 만족함으로 결국 lo + 1 = hi라는 것을 알 수 있다.

불변식이 만족하지 않는 경우, assertion을 사용하여 불변식 유지를 쉽게 할 수 있다.

귀류법

우리가 원하는 바와 반대되는 상황을 가정하고 논리를 전개해서 결론이 잘못됐음을 찾아내는 증명 기법. 대개 어떤 선택이 항상 최선임을 증명하고자 할 때 많이 이용된다.(예시 추후 추가)

비둘기집 원리

무한소수 찾기

분수 a/b가 주어질때 실수 연산을 사용하지 않고 분수를 소수형태로 출력하라.

void printDecimal(int a, int b){
	int iter = 0;
    while(a > 0) {
    	if(iter++ == 1) cout<<'.';
        cout<< a / b;
        a = (a % b) * 10;
    }
}

단순히 나누는 과정을 통해 소수를 출력하는 코드이다. 하지만 이 코드는 1/11과 같은 무한소수를 걸러낼 수 없다.

a = (a % b) * 10;

무한소수를 걸러내기 위해서는 이 부분을 주의깊게 봐야한다. 소수점 아래의 수를 출력하기 위해서 a % b를 사용하는데, 그렇게 되면 소수점 아래의 수의 범위가 [0, b)가 된다. 그러므로 무한소수의 경우 while이 b+1번 반복될때 까지 종료하지 않은 경우가 무한소수로 가정할 수 있고 a%b의 결과는 b개의 결과를 가지니 중복되는 경우가 무조건 한가지 생긴 것을 알 수 있다. 그러므로 같은 결과가 첫번째로 등장했을 때 부터 두번째로 등장할 때까지가 무한히 순환되는 순환 소수임을 알 수 있다.

구성적 증명

흔히 우리가 원하는 어떤 답이 존재한다는 사실을 증명하기 위해 사용된다.
구성적 증명은 답의 실제 예를 들거나, 답을 만드는 방법을 실제로 제시하는 방법이다.
그러므로 구성적 증명의 내용은 사실상 알고리즘을 구현하는 경우가 많다.

안정적 결혼 문제

n명의 남성과 여성이 단체 미팅에서 만났고, 모든 사람들은 자신이 원하는 상대방의 우선순위를 맘 속에 정했습니다. (전제 조건)
시간이 되어 남자 1호와 여자 1호가 짝이되었고, 남자 2호와 여자 2호가 짝이 되었습니다. 하지만 나중에 알고보니 남자 1호와 여자 2호는 자신들의 짝 보다 서로를 더 선호한다는 것을 알게 되었습니다. 이런 일이 일어나지 않도록 짝을 지어줄 수 있을까요(항상 최선의 경우로), 아니면 불가능한 경우가 있을까요?

구성적 증명의 대표 문제라고 한다. (https://en.wikipedia.org/wiki/Gale%E2%80%93Shapley_algorithm 이걸로 답이 존재한다는 사실이 증명되었다. 이건 구성적 아님)

알고리즘 설명

여성들이 모두 자신이 가장 선호하는 남성의 앞에 가서 프로포즈를 합니다. 남성이 그중 제일 마음에 드는 여성을 고르면 나머지는 다시 제 자리로 돌아갑니다.
제 자리로 돌아간 여성들은 상대에게 짝이 있는지 없는지 관계 없이 다음으로 마음에 드는 남성에게 다가가 프로포즈 합니다. 남성들은 현재 자신의 짝보다 더 맘에 드는 여성이 다가왔다면 현재의 파트너를 제 자리로 보내고 파트너를 교체합니다.
더이상 프로포즈 할 여성이 없을때 까지 2번을 반복합니다.

이 알고리즘이 답을 구할 수 있다는 것을 보이려면 항상 종료한다는 것, 모든 사람이 짝을 찾는다는 것, 짝들이 항상 안정적이라는 것이 증명이 되야한다.

항상 종료하는가?
각 여성들은 제 자리로 돌아가서 그 다음 우선순위에 있는 남성에게 프로포즈를 하러 가고, 그 과정을 N번 반복하게 된다. 전부 순서대로 프로포즈 한 다음에는 더이상 프로포즈할 남성이 없으므로, 결국 종료하게 된다.
모든 사람들이 짝을 찾는가?
한번이라도 프로포즈를 받은 남성은 무조건 짝을 찾은 경우이고, 모든 여성은 모든 남성에게 우선순위를 순서로 프로포즈를 하게 된다. 그러므로 짝을 찾지 못하는 경우의 수는 존재하지 않는다.
안정적인가?
귀류법으로 증명 가능하다. 짝이 된 두 남녀가 자신의 짝 보다 다른 사람을 좋아한다고 가정한다면 여성은 더 좋아하는 다른 사람에게 이전에 이미 프로포즈를 했을 것 이다. 하지만 더 좋아하는 다른 사람과 짝이 되지 못한 것은 더 마음에 드는 여성이 나타났기 때문이다. 그러므로 프로포즈 받았던 여성보다 마음에 들지 않는 여성과 최종적으로 짝이 되는 일은 일어날 수 없다.

백준 12022

#include <iostream>
#include <deque>
#include <vector>
#include <queue>
#include <algorithm>
using namespace std;
vector<deque<int> > v(1001);
int N, girls[1001][1001], matched[1001], check[1001];
// matched -> i번쨰 남자가 어떤 여자랑 짝인지 체크
// check -> i번째 여자가 어떤 남자랑 짝인지 체크
int main() {
    cin>>N;
    for(int i=0; i<N; i++)
        for(int j=0; j<N; j++){
            int pri; cin>>pri;
            v[i+1].push_back(pri);
        }
        // 남자 -> 여자 로 짝을 맞추기 때문에 
        // 남자를 기준으로 우선순위가 높은 여자부터 짝을 짓기 때문에 
        // 인접 리스트로 생성
    for(int i=0; i<N; i++)
        for(int j=0; j<N; j++){
            int pri; cin>>pri;
            girls[i+1][pri] = N-j;
            // 우선순위에 해당하는 숫자가 높을수록 우선순위가 높음.
        }
        // 여자가 이미 짝이 있을때 새로운 고백을 받았을떄 이전의 짝보다 우선순위가 높은지 확인해야 하기 때문에
        // 인접행렬로 상수시간에 접근할 수 있게 확인 
    
    // logic
    queue<int> q;
    for(int i=1; i<=N; i++)
        q.push(i);
    // 남자/여자 이분그래프 상의 탐색을 생각
    while(!q.empty()){
        // 처음에는 1~N까지의 모든 남자를 queue에 넣고
        // 그 후에는 짝이 지어졌다 깨진 경우 재탐색.
        int cur = q.front(); q.pop();
        while(!v[cur].empty()){
            int pri_girl = v[cur].front(); v[cur].pop_front();
            // 기존의 짝이 우선순위가 더 높은 경우
            if(girls[pri_girl][cur] < girls[pri_girl][check[pri_girl]])
                continue;
            matched[cur] = pri_girl;
            if(check[pri_girl]){
                q.push(check[pri_girl]);
                // 기존의 짝이 꺠진 경우
            }
            check[pri_girl] = cur;
            break;
        }
    }
    for(int i=1; i<=N; i++)
        cout<<matched[i]<<'\n';

}