verify/2-sat.test.cpp

View this file on GitHub
Last update: 2020-02-24 19:54:34+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

lib/functions/scc.cpp

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <bits/stdc++.h>
using namespace std;
using i64 = long;

#include "../lib/functions/scc.cpp"


signed main() {
    string p, cnf;
    int n, m;
    cin >> p >> cnf >> n >> m;
    /*
     x |  y  :  !x =>  y
     x |  y  :  !y =>  x
    !x |  y  :   x =>  y
    !x |  y  :  !y => !x
     x | !y  :   y =>  x
     x | !y  :  !x => !y
    !x | !y  :   x => !y
    !x | !y  :   y => !x
     */

    vector<vector<int>> edges(2 * n);

    for(int i = 0; i < m; ++i){
        int a, b, tmp;
        cin >> a >> b >> tmp;
        int x = abs(a) - 1;
        int y = abs(b) - 1;
        // if x_plus: true
        bool x_plus = (a >= 0);
        bool y_plus = (b >= 0);

        edges[x + (x_plus ? 0 : n)].emplace_back(y + (y_plus ? n : 0));
        edges[y + (y_plus ? 0 : n)].emplace_back(x + (x_plus ? n : 0));
    }
    auto ret = scc(edges);

    for(int i = 0; i < n; ++i){
        if(ret[i] == ret[i + n]){
            cout << "s UNSATISFIABLE" << endl;

            return 0;
        }
    }

    cout << "s SATISFIABLE" << endl;
    cout << "v";

    for(int i = 0; i < n; ++i){
        cout << " " << (ret[i] < ret[i + n] ? 1 : -1) * (i + 1);
    }
    cout << " " << 0 << endl;

}

#line 1 "verify/2-sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include <bits/stdc++.h>
using namespace std;
using i64 = long;

#line 1 "lib/functions/scc.cpp"
vector<int> scc(vector<vector<int>>& edges){
    int n = edges.size();
    vector<vector<int>> rev(n);

    for(int i = 0; i < n; ++i)
        for(auto& x : edges[i])
            rev[x].emplace_back(i);

    vector<i64> dfs_num(n, -1);
    vector<i64> flag(n, 0);
    int num = 0;
    function<void(int)> dfs = [&](int pos){
        flag[pos] = 1;
        for(auto& xx : edges[pos])
            if(!flag[xx]){
                dfs(xx);
        }
        dfs_num[pos] = num++;
    };

    for(int i = 0; i < n; ++i)
        if(!flag[i])
            dfs(i);

    vector<int> dfs_inv(n);
    for(int i = 0; i < n; ++i)
        dfs_inv[n - 1 - dfs_num[i]] = i;

    num = 0;

    vector<int> scc_vec(n, -1);

    function<void(int)> rdfs = [&](int pos){
        scc_vec[pos] = num;
        for(auto t : rev[pos])
            if(scc_vec[t] == -1)
                rdfs(t);
    };

    for(int i = 0; i < n; ++i)
        if(scc_vec[dfs_inv[i]] == -1){
            rdfs(dfs_inv[i]);
            ++num;
        }

    return scc_vec;
}
#line 8 "verify/2-sat.test.cpp"


signed main() {
    string p, cnf;
    int n, m;
    cin >> p >> cnf >> n >> m;
    /*
     x |  y  :  !x =>  y
     x |  y  :  !y =>  x
    !x |  y  :   x =>  y
    !x |  y  :  !y => !x
     x | !y  :   y =>  x
     x | !y  :  !x => !y
    !x | !y  :   x => !y
    !x | !y  :   y => !x
     */

    vector<vector<int>> edges(2 * n);

    for(int i = 0; i < m; ++i){
        int a, b, tmp;
        cin >> a >> b >> tmp;
        int x = abs(a) - 1;
        int y = abs(b) - 1;
        // if x_plus: true
        bool x_plus = (a >= 0);
        bool y_plus = (b >= 0);

        edges[x + (x_plus ? 0 : n)].emplace_back(y + (y_plus ? n : 0));
        edges[y + (y_plus ? 0 : n)].emplace_back(x + (x_plus ? n : 0));
    }
    auto ret = scc(edges);

    for(int i = 0; i < n; ++i){
        if(ret[i] == ret[i + n]){
            cout << "s UNSATISFIABLE" << endl;

            return 0;
        }
    }

    cout << "s SATISFIABLE" << endl;
    cout << "v";

    for(int i = 0; i < n; ++i){
        cout << " " << (ret[i] < ret[i + n] ? 1 : -1) * (i + 1);
    }
    cout << " " << 0 << endl;

}