mmrz's library

This documentation is automatically generated by online-judge-tools/verification-helper

---

Project maintained by mm-rz Hosted on GitHub Pages — Theme by mattgraham

2-SAT
(graph/two_sat.hpp)

• View this file on GitHub
• Last update: 2025-07-01 03:22:56+09:00
• Include: #include "graph/two_sat.hpp"

2-SAT

使い方

• two_sat(n) : コンストラクタ。$n$ は変数の数を表す
• void add_clause(int i, int f1, int j, int f2) : 句を追加する
• void add_clause(int i, int f1, int j, int f2) : 句を追加する
• void add_true(int i) : 句を追加する
• void add_false(int i) : 句を追加する
• vector<bool> solve() : 与えられた $n$ 変数 $m$ 句が充足可能か調べる。充足可能であった場合、真偽の割り当て例を $1$ つ返す。不可能な場合、空の配列を返す。 $O(N+M)$

概要

論理式の対応を有向グラフとみて、矛盾がないかをチェックする。チェックに強連結成分分解を行う部分がネックとなり、$O(N+M)$ となる。

Depends on

• 強連結成分分解 (graph/strongly_connected_components.hpp)

Verified with

• verify/aoj/id/3205.test.cpp
• verify/yosupo/two_sat.test.cpp
• verify/yukicoder/274.test.cpp

Code

#pragma once

#include "./strongly_connected_components.hpp"

struct two_sat {
	int n;
	scc_graph g;

	two_sat(int _n) : n(_n), g(scc_graph(2*n)) {}

	// (i = f1) || (j = f2)
	void add_clause(int i, bool f1, int j, bool f2){
		g.add_edge((i << 1) ^ !f1, (j << 1) ^ f2);
		g.add_edge((j << 1) ^ !f2, (i << 1) ^ f1);
	}

	// (i = f1) -> (j = f2) <=> (1 = !f1) || (j = f2)
	void add_if(int i, bool f1, int j, bool f2){
		add_clause(i, !f1, j, f2);
	}

	// i
	void set_true(int i){
		add_clause(i, true, i, true);
	}

	// !i
	void set_false(int i){
		add_clause(i, false, i, false);
	}

	std::vector<bool> solve(){
		std::vector<std::vector<int>> scc = g.scc();
		std::vector<int> c(2*n);
		for(int i = 0;i < (int)scc.size();i++){
			for(auto v : scc[i]){
				c[v] = i;
			}
		}
		std::vector<bool> res(n);
		for(int i = 0;i < n;i++){
			if(c[i << 1] == c[i << 1 | 1])return std::vector<bool>();
			res[i] = (c[i << 1] < c[i << 1 | 1]);
		}
		return res;
	}
};

#line 2 "graph/two_sat.hpp"

#line 2 "graph/strongly_connected_components.hpp"

#include<vector>

struct scc_graph {
	int n;
	int k;
	std::vector<std::vector<int>> g;
	std::vector<std::vector<int>> rg;
	std::vector<bool> used;
	std::vector<int> cmp;
	std::vector<int> vs;

	scc_graph(int _n) : n(_n), k(0), g(n), rg(n), used(n), cmp(n) {}

	void add_edge(int a, int b) {
		g[a].push_back(b);
		rg[b].push_back(a);
	}

	void dfs(int v){
		used[v] = true;
		for(auto to : g[v]){
			if(not used[to])dfs(to);
		}
		vs.push_back(v);
	}

	void rdfs(int v, int col){
		used[v] = true;
		cmp[v] = col;
		for(auto to : rg[v]){
			if(not used[to])rdfs(to, col);
		}
	}

	std::vector<std::vector<int>> scc() {
		for(int i = 0;i < n;i++){
			if(not used[i])dfs(i);
		}
		for(int i = 0;i < n;i++){
			used[i] = false;
		}
		for(auto i = vs.rbegin();i != vs.rend();i++){
			if(not used[*i])rdfs(*i, k++);
		}
		std::vector<std::vector<int>> ret(k);
		for(int i = 0;i < n;i++){
			ret[cmp[i]].push_back(i);
		}
		return ret;
	}
};
#line 4 "graph/two_sat.hpp"

struct two_sat {
	int n;
	scc_graph g;

	two_sat(int _n) : n(_n), g(scc_graph(2*n)) {}

	// (i = f1) || (j = f2)
	void add_clause(int i, bool f1, int j, bool f2){
		g.add_edge((i << 1) ^ !f1, (j << 1) ^ f2);
		g.add_edge((j << 1) ^ !f2, (i << 1) ^ f1);
	}

	// (i = f1) -> (j = f2) <=> (1 = !f1) || (j = f2)
	void add_if(int i, bool f1, int j, bool f2){
		add_clause(i, !f1, j, f2);
	}

	// i
	void set_true(int i){
		add_clause(i, true, i, true);
	}

	// !i
	void set_false(int i){
		add_clause(i, false, i, false);
	}

	std::vector<bool> solve(){
		std::vector<std::vector<int>> scc = g.scc();
		std::vector<int> c(2*n);
		for(int i = 0;i < (int)scc.size();i++){
			for(auto v : scc[i]){
				c[v] = i;
			}
		}
		std::vector<bool> res(n);
		for(int i = 0;i < n;i++){
			if(c[i << 1] == c[i << 1 | 1])return std::vector<bool>();
			res[i] = (c[i << 1] < c[i << 1 | 1]);
		}
		return res;
	}
};

Back to top page