백준16992 3-SAT

작성일 | In

문제 링크

  • http://icpc.me/16992

사용 알고리즘

  • Simulated Annealing

풀이

3-SAT 문제는 NP-Complete에 속하므로 다항 시간 안에 해결하는 알고리즘이 알려져 있지 않습니다. 적절한 휴리스틱을 이용해 문제를 풀어봅시다.

제 풀이는 기본적으로 Simulated Annealing을 사용합니다. SA에 대한 설명은 계절학교와 구글 해시코드에서 놀라운 휴리스틱 실력을 보여주었던 Ryute님의 설명으로 대신합니다.

제가 처음 시도한 풀이는 다음과 같습니다.

  1. $N, M$이 매우 작으면($M\cdot2^N \leq 3\cdot10^8$정도?) Bruteforcing으로 답을 찾는다.
  2. 최대한 다양한 상수(랜덤 시드, 볼츠만 상수, 초기 온도, 온도 변화율, 상태 전이 개수 등)를 이용해 Simulated Annealing을 시도한다.
  3. 맞은 테스트케이스의 합집합이 최대한 많은 부분을 커버하도록 코드를 잘 조합한다.

(3)은 이 문제가 BOJ에서 전체 채점 문제이고 채점 순서가 고정되어 있기 때문에 가능합니다. (3)을 실현하기 위해서는 똑같은 결과를 재현할 수 있어야 하므로, 모든 랜덤 시드는 손으로 직접 입력해야 합니다.

여기까지 오면 19x점 정도를 얻을 수 있습니다. 초기 상태를 모두 false으로 지정해서 그런지 성능이 별로 안 좋았습니다. 그래서 초기 상태를 지정하는 것도 여러 가지 방법을 시도해 보았습니다.

  • 모두 false으로 초기화 (ZeroInitializer)
  • 랜덤으로 초기화 (RandomInitializer)
  • clause에 true로 등장하는 횟수가 많으면 true, false로 등장하는 횟수가 더 많으면 false로 초기화 (StrangeInitializer)

여러 초기화 전략을 시도하니 200 ~ 203점을 받게 되었습니다. 여기까지 작성한 코드는 다음과 같습니다. 앞서 말한 것처럼, 실행 결과를 재현할 수 있도록 랜덤 시드를 직접 파라미터로 넘깁니다.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
/**
 * SimulatedAnnealing
 * @param n : number of variables
 * @param cl : clauses list
 * @param init : initial state
 * @param k : Boltzmann constant
 * @param t : initial temperature
 * @param delta : delta temperature
 * @param epoch : number of iterations
 * @param select : number of changes at one iteration
 * @param seed : random seed
 * @return : true if SA find the answer
 */
bool SimulatedAnnealing(int n, const clauses &cl, State init,
                        double k, double t, double delta, int epoch,
                        int select=1, int seed=0x917917){
    State now = init;
    int score = now.score(cl);
    Random rnd(n, seed);
    for(int iter=0; iter<epoch; iter++){
        State nxt = now;
        for(int j=0; j<select; j++) nxt.flip(rnd);
        int nxtScore = nxt.score(cl);
        if(exp((double)(nxtScore - score) / (k * t)) > rnd.next()){
            now = nxt;
            score = nxtScore;
        }
        if(score == cl.size()){
            cout << "1\n";
            now.print(n);
            return true;
        }
        t *= delta;
    }
    return false;
}
// 중략
Random R(0x917917); // Random Manager class using mt19937
if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 2, 0x482794)) return 0;
if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 1, 0x917917)) return 0;
if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 2.5, 1.0, 0.9999, 50505, 1, 0x482794)) return 0;
if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 1, 0x917917)) return 0;
if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9995, 50505, 1, 0x917917)) return 0;
if(SimulatedAnnealing(N, C, RandomInitializer(N, R) , 1.5, 5.0, 0.9999, 50505, 1, 0x917917)) return 0;
if(SimulatedAnnealing(N, C, RandomInitializer(N, R) , 1.5, 5.0, 0.9995, 50505, 1, 0x917917)) return 0;
if(SimulatedAnnealing(N, C, StrangeInitializer(N, C), 1.0, 1.5, 0.9999, 50505, 1, 0x917917)) return 0;

여기까지 오면 보통 28, 41, 128번 테스트케이스 같은 곳에서 한 두 개 정도 틀릴텐데, 이런 부분을 직접 잡는 것은 너무 힘들어서 랜덤을 믿기로 했습니다.
RandomInitializer를 이용해 초기화를 한 뒤, 처음으로 false가 되는 clause에 관여하는 변수 하나를 뒤집는 연산(flipHeuristic)을 100번 정도 수행하는 것을 시간 제한이 끝나기 직전까지 반복합니다.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
bool RandomSearch(int n, const clauses &cl, int select, double tl, int seed=0x917917){
    Random rnd(seed);
    while(clock() < tl * CLOCKS_PER_SEC){
        State now = RandomInitializer(n, rnd);
        for(int i=0; i<select; i++){
            if(now.flipHeuristic(rnd, cl)){
                cout << "1\n";
                now.print(n);
                return true;
            }
        }
    }
    return false;
}
// 중략
if(RandomSearch(N, C, 100, 1.5, 0x814814)) return 0;

RandomSearch까지 추가했더니 204개의 테스트케이스를 모두 맞을 수 있었습니다.

아래 코드는 랜덤 시드가 고정되어있기 때문에, 그대로 제출하면 글을 업로드한 2021년 9월 기준으로 모든 테스트케이스에 대해 올바른 답을 낼 수 있음이 보장됩니다.

전체 코드

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
#include <bits/stdc++.h>
using namespace std;
using clause = array<int,3>;
using clauses = vector<clause>;

struct Random{
    mt19937 gen;
    uniform_int_distribution<int> rnd_int;
    uniform_real_distribution<double> rnd_real;
    Random(int n, int seed=0x917917) : gen(seed), rnd_int(1, n), rnd_real(0, 1) {}
    int nextInt(){ return rnd_int(gen); }
    double next(){ return rnd_real(gen); }
};

struct State{
    array<int, 111> a;
    int& operator [] (int idx) { return a[idx]; }
    void flip(Random &rnd){
        a[rnd.nextInt()] ^= 1;
    }
    bool flipHeuristic(Random &rnd, const clauses &cl){
        for(const auto &[x,y,z] : cl){
            bool now = false;
            now |= x > 0 ? a[x] : !a[-x];
            now |= y > 0 ? a[y] : !a[-y];
            now |= z > 0 ? a[z] : !a[-z];
            if(!now){
                int select = rnd.gen() % 3;
                if(select == 0) a[abs(x)] ^= 1;
                if(select == 1) a[abs(y)] ^= 1;
                if(select == 2) a[abs(z)] ^= 1;
                return false;
            }
        }
        return true;
    }
    int score(const clauses &cl) const {
        int ret = 0;
        for(const auto &[x,y,z] : cl){
            bool now = false;
            now |= x > 0 ? a[x] : !a[-x];
            now |= y > 0 ? a[y] : !a[-y];
            now |= z > 0 ? a[z] : !a[-z];
            ret += now;
        }
        return ret;
    }
    void print(int n) const {
        for(int i=1; i<=n; i++) cout << a[i] << " \n"[i==n];
    }
};

State ZeroInitializer(int n){
    State ret;
    for(int i=1; i<=n; i++) ret[i] = 0;
    return ret;
}

State RandomInitializer(int n, Random &rnd){
    State ret;
    for(int i=1; i<=n; i++) ret[i] = rnd.gen() & 1;
    return ret;
}

State StrangeInitializer(int n, const clauses &cl){
    State ret;
    vector<int> sum(n+1);
    for(const auto &arr : cl){
        for(const auto &j : arr) sum[abs(j)] += j;
    }
    for(int i=1; i<=n; i++) ret[i] = sum[i] > 0;
    return ret;
}

void Naive(int n, const clauses &cl){
    State state;
    for(int i=0; i<(1<<n); i++){
        for(int j=0; j<n; j++) state[j+1] = (i & (1 << j)) != 0;
        if(state.score(cl) == cl.size()){
            cout << "1\n";
            state.print(n);
            return;
        }
    }
    cout << "0\n";
}

bool SimulatedAnnealing(int n, const clauses &cl, State init,
                        double k, double t, double delta, int epoch,
                        int select=1, int seed=0x917917){
    State now = init;
    int score = now.score(cl);
    Random rnd(n, seed);
    for(int iter=0; iter<epoch; iter++){
        State nxt = now;
        for(int j=0; j<select; j++) nxt.flip(rnd);
        int nxtScore = nxt.score(cl);
        if(exp((double)(nxtScore - score) / (k * t)) > rnd.next()){
            now = nxt;
            score = nxtScore;
        }
        if(score == cl.size()){
            cout << "1\n";
            now.print(n);
            return true;
        }
        t *= delta;
    }
    return false;
}

bool RandomSearch(int n, const clauses &cl, int select, double tl, int seed=0x917917){
    Random rnd(seed);
    while(clock() < tl * CLOCKS_PER_SEC){
        State now = RandomInitializer(n, rnd);
        for(int i=0; i<select; i++){
            if(now.flipHeuristic(rnd, cl)){
                cout << "1\n";
                now.print(n);
                return true;
            }
        }
    }
    return false;
}

int main(){
    ios_base::sync_with_stdio(false); cin.tie(nullptr);
    int N, M;
    cin >> N >> M;
    clauses C(M);
    for(auto &[x,y,z] : C) cin >> x >> y >> z;
    if(N <= 20 && (M << N) <= 3e8){ Naive(N, C); return 0; }

    Random R(0x917917);
    if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 2, 0x482794)) return 0;
    if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 1, 0x917917)) return 0;
    if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 2.5, 1.0, 0.9999, 50505, 1, 0x482794)) return 0;
    if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9999, 50505, 1, 0x917917)) return 0;
    if(SimulatedAnnealing(N, C, ZeroInitializer(N)      , 1.5, 1.0, 0.9995, 50505, 1, 0x917917)) return 0;
    if(SimulatedAnnealing(N, C, RandomInitializer(N, R) , 1.5, 5.0, 0.9999, 50505, 1, 0x917917)) return 0;
    if(SimulatedAnnealing(N, C, RandomInitializer(N, R) , 1.5, 5.0, 0.9995, 50505, 1, 0x917917)) return 0;
    if(SimulatedAnnealing(N, C, StrangeInitializer(N, C), 1.0, 1.5, 0.9999, 50505, 1, 0x917917)) return 0;
    if(RandomSearch(N, C, 100, 1.5, 0x814814)) return 0;
    cout << "0\n";
}