yukicoder No.274 The Wall 解説 - Baby Stepsなブログ

問題

yukicoder.me

2-SATについての前提

2-SAT問題の解き方

論理和を論理包含に変換
1を元にimplication graphを作る
2のimplication graphを強連結成分分解する
3の結果、ある要素Xとその否定￢Xが強連結成分であるなら、その2-SATを満たす解は存在しない

式変換について

論理包含P→Qとは、Pが偽またはQが真であることを意味する。論理包含を利用することで論理和は、以下の様に書き換えることが可能。

P∨Q ⇔ ￢P→Q∧￢Q→P

implication graphについて

論理包含をの関係をグラフにおこしたものをimplication graphと言う。

implication graphにおいて強連結である頂点の真偽値は全て等しいという性質がある。（これは参考に載せた、2-SATを解いた時のメモに解説がある）

強連結である頂点は互いに行き来可能なので、(P, Q)が強連結であるなら、P→Q∧Q→P、つまりPとQは等しい。

この性質から、もしある変数Xとその否定￢Xが同じ強連結な集合に属するなら、そのimplication graphは矛盾することになり、その2-SATには解が無い事になる。

解説

1つの区間を2-SATにおける1つの変数と捉える。また、その変数の否定とは、区間を180度回転させたものとする。

すると、ある2つの区間が重なる可能性があるなら、その2つの区間を指す変数をA, Bとして、A∨Bという論理和の関係が成り立つ。（どちらか一方しか取れないため）

全ての2頂点間について、重なる可能性があるかを見ていく。（2頂点間の関係は180度回転させる場合を加味すると4パターンあることに注意する。）

上記の論理和の関係を、論理包含に変換しimplication graphを構築する。後は前提に記述した2-SATの解き方で解ける。

解答コード

struct StronglyConnectedComponents {
  int n;
  vector<vector<int>> G, rG;
  vector<int> order, component;
  vector<bool> used;
  void dfs(int v) {
    used[v] = 1;
    for (auto nv : G[v]) {
      if (!used[nv]) dfs(nv);
    }
    order.push_back(v);
  }
  void rdfs(int v, int k) {
    component[v] = k;
    for (auto nv : rG[v]) {
      if (component[nv] < 0) rdfs(nv, k);
    }
  }

  StronglyConnectedComponents(vector<vector<int>> &_G) {
    n = _G.size();
    G = _G;
    rG.resize(n);
    component.assign(n, -1);
    used.resize(n);
    for (int v = 0; v < n; v++) {
      for (auto nv : G[v]) rG[nv].push_back(v);
    }
    for (int v = 0; v < n; v++) if (!used[v]) dfs(v);
    int k = 0;
    reverse(order.begin(), order.end());
    for (auto v : order) if (component[v] == -1) rdfs(v, k), k++;
  }

  bool is_same(int u, int v) { return component[u] == component[v]; }

  vector<vector<int>> rebuild() {
    int N = *max_element(component.begin(), component.end()) + 1;
    vector<vector<int>> rebuildedG(N);
    set<pair<int, int>> connected;
    for (int v = 0; v < N; v++) {
      for (auto nv : G[v]) {
        if (component[v] != component[nv] and !connected.count(pair(v, nv))) {
          connected.insert(pair(v, nv));
          rebuildedG[component[v]].push_back(component[nv]);
        }
      }
    }
    return rebuildedG;
  }
};

#define rep(i, n) for (long long i = (long long)(0); i < (long long)(n); ++i)
#define irep(i, m, n) for (long long i = (long long)(m); i < (long long)(n); ++i)
using ll = long long;
template<class t> using vc=vector<t>;

signed main()
{
  cin.tie( 0 ); ios::sync_with_stdio( false );
  
  int n,m; cin>>n>>m;
  vc<int> l(n), r(n);
  rep(i,n) cin>>l[i]>>r[i];
  
  vc<vc<int>> G(2*n);
  rep(i,n){
    irep(j,i+1,n){
      int l1=l[i], r1=r[i], l2=l[j], r2=r[j];
      int L1=m-r1-1, R1=m-l1-1, L2=m-r2-1, R2=m-l2-1;
      if(l1<=l2 and l2<=r1 or l1<=r2 and r2<=r1
        or l2<=l1 and l1<=r2){
        // A∨B <=> ￢A=>B∧￢B=>A
        G[i+n].push_back(j);
        G[j+n].push_back(i);
      }
      if(l1<=L2 and L2<=r1 or l1<=R2 and R2<=r1
        or L2<=l1 and l1<=R2){
        // A∨￢B <=> ￢A=>￢B∧B=>A
        G[i+n].push_back(j+n);
        G[j].push_back(i);
      }
      if(L1<=l2 and l2<=R1 or L1<=r2 and r2<=R1
        or l2<=L1 and L1<=r2){
        // ￢A∨B <=> A=>B∧￢B=>￢A
        G[i].push_back(j);
        G[j+n].push_back(i+n);
      }
      if(L1<=L2 and L2<=R1 or L1<=R2 and R2<=R1
        or L2<=L1 and L1<=R2){
        // ￢A∨￢B <=> A=>￢B∧B=>￢A
        G[i].push_back(j+n);
        G[j].push_back(i+n);
      }
    }
  }
  
  auto scc = StronglyConnectedComponents(G);
  rep(i,n){
    if(scc.is_same(i,i+n)){
      cout<<"NO"<<endl;
      return 0;
    }
  }
  cout<<"YES"<<endl;
}

参考

japlj.hatenadiary.org

論理包含に関する解説

applelife100.blogspot.com