Verify/LC_two_sat.test.cpp

View this file on GitHub
Last update: 2024-04-26 03:18:17+09:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

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

#include "Template/template.hpp"

#include "Math/twosat.hpp"


int main(){
    string tmp;
    int n,m; cin>>tmp>>tmp>>n>>m;
    TwoSat ts(n+1);
    rep(i,0,m){
        int a,b; cin>>a>>b>>tmp;
        ts.either(abs(a),a>0,abs(b),b>0);
    }
    if(!ts.satisfiable()){
        puts("s UNSATISFIABLE");
        return 0;
    }
    puts("s SATISFIABLE");
    cout<<"v ";
    auto res=ts.res;
    rep(i,1,n+1){
        if(res[i])cout<<i<<' ';
        else cout<<-i<<' ';
    }
    puts("0");
    return 0;
}

#line 1 "Verify/LC_two_sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#line 1 "Template/template.hpp"
#include <bits/stdc++.h>

using namespace std;

#define rep(i, a, b) for (int i = (int)(a); i < (int)(b); i++)
#define rrep(i, a, b) for (int i = (int)(b-1); i >= (int)(a); i--)
#define ALL(v) (v).begin(), (v).end()
#define UNIQUE(v) sort(ALL(v)), (v).erase(unique(ALL(v)), (v).end())
#define SZ(v) (int)v.size()
#define MIN(v) *min_element(ALL(v))
#define MAX(v) *max_element(ALL(v))
#define LB(v, x) int(lower_bound(ALL(v), (x)) - (v).begin())
#define UB(v, x) int(upper_bound(ALL(v), (x)) - (v).begin())

using uint = unsigned int;
using ll = long long int;
using ull = unsigned long long;
using i128 = __int128_t;
using u128 = __uint128_t;
const int inf = 0x3fffffff;
const ll INF = 0x1fffffffffffffff;

template <typename T> inline bool chmax(T &a, T b) {
    if (a < b) {
        a = b;
        return 1;
    }
    return 0;
}
template <typename T> inline bool chmin(T &a, T b) {
    if (a > b) {
        a = b;
        return 1;
    }
    return 0;
}
template <typename T, typename U> T ceil(T x, U y) {
    assert(y != 0);
    if (y < 0)
        x = -x, y = -y;
    return (x > 0 ? (x + y - 1) / y : x / y);
}
template <typename T, typename U> T floor(T x, U y) {
    assert(y != 0);
    if (y < 0)
        x = -x, y = -y;
    return (x > 0 ? x / y : (x - y + 1) / y);
}
template <typename T> int popcnt(T x) {
    return __builtin_popcountll(x);
}
template <typename T> int topbit(T x) {
    return (x == 0 ? -1 : 63 - __builtin_clzll(x));
}
template <typename T> int lowbit(T x) {
    return (x == 0 ? -1 : __builtin_ctzll(x));
}

#ifdef LOCAL
#define show(...) _show(0, #__VA_ARGS__, __VA_ARGS__)
#else
#define show(...) true
#endif
template <typename T> void _show(int i, T name) {
    cerr << '\n';
}
template <typename T1, typename T2, typename... T3>
void _show(int i, const T1 &a, const T2 &b, const T3 &...c) {
    for (; a[i] != ',' && a[i] != '\0'; i++)
        cerr << a[i];
    cerr << ":" << b << " ";
    _show(i + 1, a, c...);
}
template <class T, class U>
ostream &operator<<(ostream &os, const pair<T, U> &p) {
    os << "P(" << p.first << ", " << p.second << ")";
    return os;
}
template <typename T, template <class> class C>
ostream &operator<<(ostream &os, const C<T> &v) {
    os << "[";
    for (auto d : v)
        os << d << ", ";
    os << "]";
    return os;
}
#line 2 "Graph/scc.hpp"

struct SCC{
    int n,m,cur;
    vector<vector<int>> g;
    vector<int> low,ord,id;
    SCC(int _n=0):n(_n),m(0),cur(0),g(_n),low(_n),ord(_n,-1),id(_n){}
    void resize(int _n){
        n=_n;
        g.resize(n);
        low.resize(n);
        ord.resize(n,-1);
        id.resize(n);
    }
    void add_edge(int u,int v){g[u].emplace_back(v);}
    void dfs(int v,vector<int>& used){
        ord[v]=low[v]=cur++;
        used.emplace_back(v);
        for(auto& nxt:g[v]){
            if(ord[nxt]==-1){
                dfs(nxt,used); chmin(low[v],low[nxt]);
            }
            else{
                chmin(low[v],ord[nxt]);
            }
        }
        if(ord[v]==low[v]){
            while(1){
                int add=used.back(); used.pop_back();
                ord[add]=n; id[add]=m;
                if(v==add)break;
            }
            m++;
        }
    }
    void run(){
        vector<int> used;
        rep(v,0,n)if(ord[v]==-1)dfs(v,used);
        for(auto& x:id)x=m-1-x;
    }
};

/**
 * @brief Strongly Connected Components
 */
#line 3 "Math/twosat.hpp"

struct TwoSat{
    int n;
    vector<bool> res;
    SCC graph;
    TwoSat(int _n):n(_n),res(n),graph(n*2){}
    void add(int x){
        n+=x;
        res.resize(n);
        graph.resize(n*2);
    }
    void either(int i,bool f,int j,bool g){
        graph.add_edge(2*i+(f^1),2*j+g);
        graph.add_edge(2*j+(g^1),2*i+f);
    }
    void AtMostOne(vector<int>& a){
        int offset=n;
        add(a.size());
        rep(i,0,a.size())either(a[i],0,offset+i,1);
        rep(i,1,a.size())either(offset+i-1,0,offset+i,1);
        rep(i,1,a.size())either(a[i],0,offset+i-1,0);
    }
    bool satisfiable(){
        graph.run();
        auto id=graph.id;
        rep(i,0,n){
            if(id[i*2]==id[i*2+1])return false;
            res[i]=id[i*2]<id[i*2+1];
        }
        return true;
    }
};

/**
 * @brief 2-SAT
 */
#line 5 "Verify/LC_two_sat.test.cpp"

int main(){
    string tmp;
    int n,m; cin>>tmp>>tmp>>n>>m;
    TwoSat ts(n+1);
    rep(i,0,m){
        int a,b; cin>>a>>b>>tmp;
        ts.either(abs(a),a>0,abs(b),b>0);
    }
    if(!ts.satisfiable()){
        puts("s UNSATISFIABLE");
        return 0;
    }
    puts("s SATISFIABLE");
    cout<<"v ";
    auto res=ts.res;
    rep(i,1,n+1){
        if(res[i])cout<<i<<' ';
        else cout<<-i<<' ';
    }
    puts("0");
    return 0;
}