2-SAT(2-CNF Satisfiability Problem)

여기, 여기, 여기, 여기 참조

수학적인 기초

먼저 절, 명제, 조건문 이 세가지가 헷갈리기 쉬운데, 이 알고리즘을 이해하려면 절대 헷갈리면 안된다.

절은 나중에 설명하고 명제부터 살펴보자.

명제란 대한민국의 수도는 서울이다, 사람은 날 수 있다. 처럼 true/false를 특정지을 수 있는 것을 말한다. 

나는 사람이다. 라는 명제를 P로 놓고, 나는 동물이다. 라는 명제를 Q로 놓은 다음 화살표로 연결하면

P->Q 이렇게 되고 조건문이된다.

조건문의 true/false는 생각보다 까다로운데 명제논리 링크를 참조해서 이해해보자.

P	Q	P → Q
T	T	T
T	F	F
F	T	T
F	F	T

위에서 다른건 다 상식선에서 이해가 되는데 P가 거짓이면 Q가 참이던 거짓이던 모순이 없는건 일상생활 명제에 대입하면 좀 받아들이기 힘들다.

(철희가 남자라면 철희는 남자가 아니다. 라는 조건문도 모순이 없는 참이 되어버리는 사태가 발생한다. 근데 생각해보면 남자라면 이라는게 거짓일때만 모순이 없는것이므로, 남자라는게 뻥이었으므로 뻥이 아닌 사실로는 남자일수도 있고 아닐수도 있는 상태가 되는걸로 이해는 가능하다. )

그럴때는 다음 문장을 참고해서 대략적으로 이해하고 넘어가자

P가 거짓일 때 참이되는 것이 아직 받아들이기 어렵다면 이렇게 생각해보자. 선생님이 학생에게 '체육대회에서 100m를 5초안에 뛸 수 있으면 72 km/h... 아이스크림을 주겠다'라고 말했다고 해보자. 이 말이 거짓말이 되는 경우는 "단 한가지" 뿐이다. 즉, (2) 학생이 100m를 5초 안에 들어왔는데 선생님이 아이스크림 안주는 경우만 거짓이다. (3) 학생이 5초안에 못뛰었을 때 선생님이 학생이 안쓰러워 아이스크림을 사준 경우 이는 선생님이 약속을 어겼다고 볼 수 없고 단순한 변심으로 보는게 타당할 것이다. 즉 위의 선생님의 약속(가언 명제) 자체는 여전히 참이다. 그리고 마찬가지로 (4) 5초안에 못뛰었을 때 선생님이 아이스크림을 사주지 않는 경우 학생은 그런가보다 하고 넘어갈 수 있고 이 또한 선생님이 약속(가언 명제)을 어겼다고 할 수 없다. 즉, 참으로 인정한다. 다시 정리하자면 학생이 100m를 5초 안에 뛰지 못한 경우에 대해서 선생님은 어떠한 약속도 하지않았으므로 선생님이 어떤 행동을 하든 약속이 거짓말이 될 수없다.[12]

2SAT이란

2-SAT(2-SATisfiability)문제는 충족 가능성 문제(satisfiability problem)의 한 종류입니다.

충족 가능성 문제란, 여러 개의 boolean변수들로 이루어진 식이 있을 때 각 변수에 값을 할당하여 식을 참으로 만드는 조합을 찾거나, 그러한 조합이 없음을 찾는 문제입니다.

f = (x2 ∨ ￢x1) ∧ (￢x1 ∨ ￢x2) ∧ (x1 ∨ x3) ∧ (￢x2 ∨ ￢x3) ∧ (x1 ∨ x4)

이 식은 {x1 : false, x2 : false, x3 : true, x4 : true} 인 경우에 참이 됩니다.

가만 보면, 나이브한 솔루션은  x1~x4값에 대해서 0과1을 대입해보는 식으로 2^n의 모든 부분집합을 테스트해보면 된다는 사실을 알 수 있다. 

위에보면 괄호안에 두개의 변수가 들어있는데, 그래서 2-SAT이고, 괄호하나를 절(clause)이라고 부른다.

괄호안은 항상 OR 연산자, 괄호밖은 항상 AND연산자로 되어 있다. 

이렇게 절의 AND 연산으로만 표현된 식의 형태를 CNF(Conjunctive Normal Form)라고 합니다.

1SAT문제는 트리비얼하게 O(N)에 풀린다.

3SAT이상은 다항시간 솔루션이 없다.

신기하게도 2SAT문제도 선형시간에 풀린다!

여기까지만 들으면 이런걸 왜 보고 있나하는 생각이 드는데, 의외로 많은 문제들이 2-SAT으로 변환 가능하고, SCC로 풀수 있다고 한다.

여기 참조

1. 답이 존재하는지 여부 구하기

여기까지는 할만한 느낌

핵심아이디어

1. 논리식을 조건문으로 바꾼다 : (A∨B) = ¬A → B 와 ¬B → A  !!

A가 거짓이라면 B는 무조건 참이여야 하며, B가 거짓이라면 A는 무조건 참이여야 한다.

2. 모든 절의 명제들을 합하여 하나의 유향그래프를 생성할 수 있다.

3. 사이클 전체가 true이거나 전체가 false로 통일되어야한다. A와 ¬A이 같은 사이클에 있을 수 없다.

P	Q	P → Q
T	T	T
T	F	F
F	T	T
F	F	T

3번을 잘 이해해야 하는데, true -> false이면(사실 그럴때만) 조건문에 모순이 생긴다는 걸 기억하면 된다.

(p → q에서 p가 참일 때는 q는 무조건 참이여야하며 p가 거짓일 때는 q가 무엇이든지 상관없음)

따라서, A→¬A가 나오면 A는 반드시 false여야 한다.

마찬가지로 ¬A→A가 나오면 A는 반드시 true여야 함

근데 (하나의 사이클에서 ) A→¬A도 발견되고 ¬A→A도 발견된다? 그럼 false도 될수 없고, true도 될수 없어서 모순!

(여기서 한가지 중요한 관찰은 같은 SCC가 아니면서 A→¬A 또는 ¬A→A 이렇게 단방향은 있을 수 있다는 것이다. 일상언어 조건문으로 바꾸면 남자이면 남자가 아니다. 이런게 되어서 무지 이상하지만, 상단에 서술했듯이 수학적으로는 모순이 없다. 조건문 왼쪽에 거짓이기만 한다면.)

내 코드는 다음과 같다. 이 문제의 답안이기도 하다.

#include <bits/stdc++.h>
using namespace std;
#define REP(i,n) for(int i=0;i<(int)(n);i++)
#define REP1(i,n) for(int i=1;i<=(int)(n);i++)
using vi = vector<int>;
using vvi = vector<vi>;
 
struct result { vi scc_map;  vvi scc_list; vvi scc_adj_list; };
result scc_dag_kosaraju(int max_v, vvi& adj_list, vvi& adj_rlist, int base1)
{
    // step1. dfs로 방문하며 말단부터 stack push
    vi visit(max_v + base1); stack<int> S;
    function<void(int n)> dfs = [&](int n) {
        if (visit[n]) return;
        visit[n] = 1;
        for (int a : adj_list[n]) dfs(a);
        S.push(n);
    };
    for (int i = base1; i < max_v + base1; i++) if (visit[i] == 0) dfs(i);
    // step2. stack에서 꺼내면서
    // 역방향으로 접근가능한 정점들을 SCC로 판정
    visit.clear(); visit.resize(max_v + base1);
    vi scc(max_v + base1);  // map. scc[v]=1 이면 v정점은 1번 SCC에 속한다고 하는것
    int scc_ix = base1;
    vvi scc_list; if (base1) scc_list.push_back(vi());
    while (S.size()) {
        int n = S.top(); S.pop();
        if (visit[n]) continue;
        vi sl;
        function<void(int n)> dfs = [&](int n) {
            if (visit[n]) return;
            visit[n] = 1;
            scc[n] = scc_ix;
            sl.push_back(n);
            for (auto a : adj_rlist[n]) dfs(a);
        };
        dfs(n);
        scc_list.push_back(sl);
        scc_ix++;
    }
    vvi scc_adj_list(scc_ix);
    for (int u = base1; u < max_v + base1; u++) {
        for (auto v : adj_list[u]) {
            if (scc[u] != scc[v]) {
                //cout << scc[u] << ' ' << scc[v] << endl;
                scc_adj_list[scc[u]].push_back(scc[v]);
            }
        }
    }
    return { scc, scc_list, scc_adj_list};
}
int32_t main()
{
    ios::sync_with_stdio(false); cin.tie(0);
    int N, M; cin >> N >> M;
    vvi adj_list(2*N + 2), adj_list2(2*N + 2);
    for(int i=0;i<M;i++) {
        int a, b; cin >> a >> b;
        if (a < 0) a *= -2; else a = a * 2 - 1;
        if (b < 0) b *= -2; else b = b * 2 - 1;
        int na = (a % 2 == 0) ? a - 1 : a + 1;
        int nb = (b % 2 == 0) ? b - 1 : b + 1;
        //not a -> b
        adj_list[na].push_back(b);
        adj_list2[b].push_back(na); // 역방향
 
        //not b -> a
        adj_list[nb].push_back(a);
        adj_list2[a].push_back(nb); // 역방향
    }
    auto r = scc_dag_kosaraju(N*2+1, adj_list, adj_list2, true);
    int ok = 1;
    for(int i=1;i<=N;i++)
    {
        if (r.scc_map[i * 2] == r.scc_map[i * 2 - 1]) ok = 0;
    }
    cout << ok << '\n';;
    return 0;
}

2. 유효한 변수값들 구하기

난이도가 확 올라가는 느낌

여기, 여기 참조

추가로 필요한 아이디어

모든 정점에 대해서 위상정렬 순으로 처음만나면 거짓을 만들어주는식으로 채워주면 된다.

예를 들어 위상정렬순으로 not X3을 먼저 만났으면 not X3 = false 가 되어야 하므로 X3은 true로 확정해주는 식.

이런방법 말고도 굉장히 많은 방법이 있는것 같은데, 적당히 한가지로 외워두면 될듯하다.

아래는 내 코드고, 이 문제에 대한 답안이기도 하다.

#include <bits/stdc++.h>
using namespace std;
#define REP(i,n) for(int i=0;i<(int)(n);i++)
#define REP1(i,n) for(int i=1;i<=(int)(n);i++)
using vi = vector<int>;
using vvi = vector<vi>;
 
struct result { vi scc_map;  vvi scc_list; };
result scc_dag_tarjan(vvi& adj_list, int base1)
{
    int max_v = (int)adj_list.size() - 1;  // base1==0일때 테스트 안됨!
    //타잔은 수행후 SCC들이 역순으로 위상정렬을 이루므로,
    //그 성질을 이용하면 좋다(2-SAT등)
 
    vvi ans;
    stack<int> S;
    //아래에서 visit는 ord와 통합가능하지만, 가독성을 위해 남겨둠
    vi scc_map(max_v + base1, -1), visit(max_v + base1), ord(max_v + base1), parent(max_v + base1); int g_ix = 0;
    // 코사라주나 단절선 구하는것과 다르게 finish 운영해줌
    // 일반적으로 finish배열이 dfs리턴할때 true해주는것과 다르게
    // SCC분리가 끝났음을 의미
    vi finish(max_v + base1);
    static int scc_ix = base1;
    function<int(int)> dfs = [&](int n)-> int  // low를 리턴
    {
        visit[n] = 1;
        ord[n] = ++g_ix;
        int low = ord[n];
        S.push(n);  // 스택에 먼저 푸시
        for (auto adj : adj_list[n])
        {
            if (visit[adj] == 0)  // tree edge 의 경우
            {
                int r = dfs(adj);
                // 단절점 로직의 경우 여기서 자식트리중 하나라도 자신위로 올라가지 못하면 단절점으로 판정하지만
                // SCC 타잔에서는 그러한 로직은 없고, 루프하단에 result == ord[n] 으로
                // 자신포함 자식트리중 도달가능한 가장 높은 정점이 자신일 경우 SCC 추출하는 로직으로 바뀐다.
                // if (r > ord[n]) ans.insert({ min(n,adj), max(n,adj) });
                low = min(low, r);
            }
            // 방문은 했으나 아직 SCC로 추출되지는 않은 이웃
            else if (finish[adj] == 0)  // back edge 또는 cross edge의 일부
                low = min(low, ord[adj]);  // 접근가능한 백정점 순서로 업데이트
        }
        // 자신포함 자식트리중 도달가능한 가장 높은 정점이 자신일 경우 SCC 추출
        if (low == ord[n])
        {
            vi scc;
            while (S.size())
            {
                int a = S.top(); S.pop();
                scc.push_back(a);
                scc_map[a] = scc_ix;
                finish[a] = 1;
                if (a == n) break;
            }
            sort(scc.begin(), scc.end());
            ans.push_back(scc);
            scc_ix++;
        }
 
        return low;
    };
    for (int i = base1; i < max_v + base1; i++) if (visit[i] == 0) dfs(i);
    return { scc_map, ans };
}
 
#define DBL(a) (2*(a))
#define CONV(a) (a)<0?(a)*-2:(a)*2+1
int32_t main()
{
    ios::sync_with_stdio(false); cin.tie(0);
 
    int N, M; cin >> N >> M;
    vvi adj_list(DBL(N+1));
    for (int i = 0; i < M; i++) {
        int a, b; cin >> a >> b;
        a = CONV(a);
        b = CONV(b);
 
        //nice magic property!
        int na = a ^ 1;
        int nb = b ^ 1;
 
        //not a -> b
        adj_list[na].push_back(b);
 
        //not b -> a
        adj_list[nb].push_back(a);
    }
    auto r = scc_dag_tarjan(adj_list, true);
    for (int i = 1; i <= N; i++)
    {
        if (r.scc_map[CONV(i)] == r.scc_map[CONV(-i)]) { cout << 0 << '\n'; return 0; }
    }
    // 여기까지 오면 변수조합이 있는건 보장된다. 모순만 없도록 배열해주면 됨
    cout << 1 << '\n';
    for (int i = 1; i <= N; i++) {
        // 아랫부분 아직 제대로 이해 못한 상태 ㅠ
        // 소스가 워낙 간결해서 일단 채택은 해 두었다.
        cout << (r.scc_map[CONV(i)] < r.scc_map[CONV(-i)]) << ' ';  
    }
    return 0;
}