verify/yosupo/other/two_sat.test.cpp

View this file on GitHub
Last update: 2025-04-16 16:10:29+07:00
Problem: https://judge.yosupo.jp/problem/two_sat

Depends on

Code

#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#include "template.hpp"
#include "graph/twosat.hpp"

int main(){
    cin.tie(nullptr)->sync_with_stdio(false);
    string s;
    int n,m;
    cin >> s >> s >> n >> m;
    TwoSAT sat(n);
    for(int i=0;i<m;i++){
        int a,b,x;
        cin >> a >> b >> x;
        sat.add_clause(abs(a)-1,a<0,abs(b)-1,b<0);
    }
    auto [ok,ans]=sat.solve();
    if(ok){
        cout << "s SATISFIABLE\n";
        cout << "v ";
        for(int i=0;i<n;i++)cout << (ans[i]?i+1:-(i+1)) << " ";
        cout << "0\n";

    }else{
        cout << "s UNSATISFIABLE\n";
    }
}

#line 1 "verify/yosupo/other/two_sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#line 2 "template.hpp"
#include<bits/stdc++.h>
#include<ext/pb_ds/assoc_container.hpp>
#include<ext/pb_ds/tree_policy.hpp>

using namespace std;
using namespace __gnu_pbds;

using ll = long long;
using db = long double;
using vi = vector<int>;
using vl = vector<ll>;
using vd = vector<db>;
using pii = pair<int,int>;
using pll = pair<ll,ll>;
using pdd = pair<db,db>;
const int INF=INT_MAX/2;
const int MOD=998244353;
const int MOD2=1000000007;
const ll LINF=LLONG_MAX/2;
const db DINF=numeric_limits<db>::infinity();
const db EPS=1e-9;
const db PI=acos(db(-1));

template<class T>
using ordered_set = tree<T,null_type,less<T>,rb_tree_tag,tree_order_statistics_node_update>;
template<class T>
using ordered_multiset = tree<T,null_type,less_equal<T>,rb_tree_tag,tree_order_statistics_node_update>;

mt19937 rng(chrono::steady_clock::now().time_since_epoch().count());
mt19937_64 rng64(chrono::steady_clock::now().time_since_epoch().count());
#line 3 "graph/twosat.hpp"

/**
 * Author: Teetat T.
 * Date: 2025-02-20
 * Description: Cartesian Tree.
 */

struct TwoSAT{
    int n;
    vector<vector<int>> adj,rev;
    TwoSAT(int _n):n(_n),adj(n*2),rev(n*2){}
    void add_edge(int u,int v){
        adj[u].emplace_back(v);
        rev[v].emplace_back(u);
    }
    void add_clause(int u,bool nu,int v,bool nv){
        u=(u<<1)|nu,v=(v<<1)|nv;
        add_edge(u^1,v);
        add_edge(v^1,u);
    }
    pair<bool,vector<bool>> solve(){
        vector<bool> vis(n*2),ans(n);
        vector<int> ord,scc(n*2);
        int scc_id=0;
        function<void(int)> dfs=[&](int u){
            if(vis[u])return;
            vis[u]=true;
            for(auto v:adj[u])dfs(v);
            ord.emplace_back(u);
        };
        function<void(int)> dfs2=[&](int u){
            if(scc[u])return;
            scc[u]=scc_id;
            for(auto v:rev[u])dfs2(v);
        };
        for(int i=0;i<2*n;i++)dfs(i);
        reverse(ord.begin(),ord.end());
        for(int i:ord)if(!scc[i]){
            scc_id++;
            dfs2(i);
        }
        for(int i=0;i<n;i++){
            if(scc[i<<1]==scc[(i<<1)|1])return {false,ans};
            ans[i]=scc[i<<1]>scc[(i<<1)|1];
        }
        return {true,ans};
    }
};
#line 4 "verify/yosupo/other/two_sat.test.cpp"

int main(){
    cin.tie(nullptr)->sync_with_stdio(false);
    string s;
    int n,m;
    cin >> s >> s >> n >> m;
    TwoSAT sat(n);
    for(int i=0;i<m;i++){
        int a,b,x;
        cin >> a >> b >> x;
        sat.add_clause(abs(a)-1,a<0,abs(b)-1,b<0);
    }
    auto [ok,ans]=sat.solve();
    if(ok){
        cout << "s SATISFIABLE\n";
        cout << "v ";
        for(int i=0;i<n;i++)cout << (ans[i]?i+1:-(i+1)) << " ";
        cout << "0\n";

    }else{
        cout << "s UNSATISFIABLE\n";
    }
}