2-SAT
(include/emthrm/misc/2-sat.hpp)

• View this file on GitHub
• Last update: 2022-12-15 22:18:37+09:00
• Include: #include "emthrm/misc/2-sat.hpp"

節内のリテラル数が高々 $2$ である連言標準形の充足可能性を判定する問題である。

時間計算量

$N$ 変数 $M$ 節 のとき $O(N + M)$

仕様

struct TwoSat;

メンバ関数

名前	効果・戻り値
explicit TwoSat(const int n);	$N$ 変数のオブジェクトを構築する。
int negate(const int x) const;	$\neg x$ を表す頂点番号
void add_or(const int x, const int y);	$x \vee y$ を追加する。
void add_if(const int x, const int y);	$x \Rightarrow y$ を追加する。
void add_nand(const int x, const int y);	$\neg (x \land y)$ を追加する。
void set_true(const int x);	$x$ を真とする。
void set_false(const int x);	$x$ を偽とする。
std::vector<bool> build();	変数の真理値。ただし矛盾が生じるときは空配列を返す。

参考文献

• Bengt Aspvall, Michael F. Plass, and Robert Endre Tarjan: A linear-time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters, Vol. 8, No. 3, pp. 121–123 (1979). https://doi.org/10.1016/0020-0190(79)90002-4
• 秋葉拓哉，岩田陽一，北川宜稔：プログラミングコンテストチャレンジブック [第2版]，pp.288-290，マイナビ出版（2012）
• https://github.com/beet-aizu/library/blob/346558ee0881bd18b10c0d32d7678b033d6b0326/graph/stronglyconnectedcomponent.cpp

Submissons

• https://judge.yosupo.jp/submission/2711

Verified with

• その他/2-SAT (test/misc/2-sat.test.cpp)

Code

#ifndef EMTHRM_MISC_2_SAT_HPP_
#define EMTHRM_MISC_2_SAT_HPP_

#include <algorithm>
#include <vector>

namespace emthrm {

struct TwoSat {
  explicit TwoSat(const int n)
      : n(n), graph(n << 1), rgraph(n << 1), is_visited(n << 1), ids(n << 1) {
    order.reserve(n << 1);
  }

  int negate(const int x) const { return (n + x) % (n << 1); }

  void add_or(const int x, const int y) {
    graph[negate(x)].emplace_back(y);
    graph[negate(y)].emplace_back(x);
    rgraph[y].emplace_back(negate(x));
    rgraph[x].emplace_back(negate(y));
  }

  void add_if(const int x, const int y) { add_or(negate(x), y); }

  void add_nand(const int x, const int y) { add_or(negate(x), negate(y)); }

  void set_true(const int x) { add_or(x, x); }

  void set_false(const int x) { set_true(negate(x)); }

  std::vector<bool> build() {
    std::fill(is_visited.begin(), is_visited.end(), false);
    std::fill(ids.begin(), ids.end(), -1);
    order.clear();
    for (int i = 0; i < (n << 1); ++i) {
      if (!is_visited[i]) dfs(i);
    }
    for (int i = (n << 1) - 1, id = 0; i >= 0; --i) {
      if (ids[order[i]] == -1) rdfs(order[i], id++);
    }
    std::vector<bool> res(n);
    for (int i = 0; i < n; ++i) {
      if (ids[i] == ids[negate(i)]) return {};
      res[i] = ids[negate(i)] < ids[i];
    }
    return res;
  }

 private:
  const int n;
  std::vector<std::vector<int>> graph, rgraph;
  std::vector<bool> is_visited;
  std::vector<int> ids, order;

  void dfs(const int ver) {
    is_visited[ver] = true;
    for (const int dst : graph[ver]) {
      if (!is_visited[dst]) dfs(dst);
    }
    order.emplace_back(ver);
  }

  void rdfs(const int ver, const int cur_id) {
    ids[ver] = cur_id;
    for (const int dst : rgraph[ver]) {
      if (ids[dst] == -1) rdfs(dst, cur_id);
    }
  }
};

}  // namespace emthrm

#endif  // EMTHRM_MISC_2_SAT_HPP_

#line 1 "include/emthrm/misc/2-sat.hpp"



#include <algorithm>
#include <vector>

namespace emthrm {

struct TwoSat {
  explicit TwoSat(const int n)
      : n(n), graph(n << 1), rgraph(n << 1), is_visited(n << 1), ids(n << 1) {
    order.reserve(n << 1);
  }

  int negate(const int x) const { return (n + x) % (n << 1); }

  void add_or(const int x, const int y) {
    graph[negate(x)].emplace_back(y);
    graph[negate(y)].emplace_back(x);
    rgraph[y].emplace_back(negate(x));
    rgraph[x].emplace_back(negate(y));
  }

  void add_if(const int x, const int y) { add_or(negate(x), y); }

  void add_nand(const int x, const int y) { add_or(negate(x), negate(y)); }

  void set_true(const int x) { add_or(x, x); }

  void set_false(const int x) { set_true(negate(x)); }

  std::vector<bool> build() {
    std::fill(is_visited.begin(), is_visited.end(), false);
    std::fill(ids.begin(), ids.end(), -1);
    order.clear();
    for (int i = 0; i < (n << 1); ++i) {
      if (!is_visited[i]) dfs(i);
    }
    for (int i = (n << 1) - 1, id = 0; i >= 0; --i) {
      if (ids[order[i]] == -1) rdfs(order[i], id++);
    }
    std::vector<bool> res(n);
    for (int i = 0; i < n; ++i) {
      if (ids[i] == ids[negate(i)]) return {};
      res[i] = ids[negate(i)] < ids[i];
    }
    return res;
  }

 private:
  const int n;
  std::vector<std::vector<int>> graph, rgraph;
  std::vector<bool> is_visited;
  std::vector<int> ids, order;

  void dfs(const int ver) {
    is_visited[ver] = true;
    for (const int dst : graph[ver]) {
      if (!is_visited[dst]) dfs(dst);
    }
    order.emplace_back(ver);
  }

  void rdfs(const int ver, const int cur_id) {
    ids[ver] = cur_id;
    for (const int dst : rgraph[ver]) {
      if (ids[dst] == -1) rdfs(dst, cur_id);
    }
  }
};

}  // namespace emthrm

Back to top page