2-SAT
(Math/twosat.hpp)

• View this file on GitHub
• Last update: 2022-01-05 16:50:26+09:00
• Include: #include "Math/twosat.hpp"

Depends on

• Strongly Connected Components (Graph/scc.hpp)

Verified with

• Verify/LC_two_sat.test.cpp

Code

#pragma once
#include "Graph/scc.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 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
 */

Back to top page