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

:heavy_check_mark: verify/yosupo/two_sat.test.cpp

Depends on

Code

# define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#include "./../../template/template.hpp"
#include "./../../graph/two_sat.hpp"

void mmrz::solve(){
	char _p;
	string _cnf;
	int n, m;
	cin >> _p >> _cnf >> n >> m;

	auto f = [](int x) -> pair<int, bool> {
		bool tf = (x > 0 ? true : false);
		x = abs(x)-1;
		return make_pair(x, tf);
	};

	two_sat ts(n);
	while(m--){
		int x, y, _zero;
		cin >> x >> y >> _zero;
		auto [nx, x_tf] = f(x);
		auto [ny, y_tf] = f(y);
		ts.add_clause(nx, x_tf, ny, y_tf);
	}

	auto ret = ts.solve();
	if(ret.empty()){
		cout << "s UNSATISFIABLE" << '\n';
		return;
	}
	cout << "s SATISFIABLE" << '\n';
	cout << "v";
	rep(i, n){
		cout << " " << (ret[i] ? "" : "-") << i+1;
	}
	cout << " 0" << '\n';
}
#line 1 "verify/yosupo/two_sat.test.cpp"
# define PROBLEM "https://judge.yosupo.jp/problem/two_sat"

#line 1 "template/template.hpp"
# include <bits/stdc++.h>
using namespace std;
using ll = long long;
using ull = unsigned long long;
const double pi = acos(-1);
template<class T>constexpr T inf() { return ::std::numeric_limits<T>::max(); }
template<class T>constexpr T hinf() { return inf<T>() / 2; }
template <typename T_char>T_char TL(T_char cX) { return tolower(cX); }
template <typename T_char>T_char TU(T_char cX) { return toupper(cX); }
template<class T> bool chmin(T& a,T b) { if(a > b){a = b; return true;} return false; }
template<class T> bool chmax(T& a,T b) { if(a < b){a = b; return true;} return false; }
int popcnt(unsigned long long n) { int cnt = 0; for (int i = 0; i < 64; i++)if ((n >> i) & 1)cnt++; return cnt; }
int d_sum(ll n) { int ret = 0; while (n > 0) { ret += n % 10; n /= 10; }return ret; }
int d_cnt(ll n) { int ret = 0; while (n > 0) { ret++; n /= 10; }return ret; }
ll gcd(ll a, ll b) { if (b == 0)return a; return gcd(b, a%b); };
ll lcm(ll a, ll b) { ll g = gcd(a, b); return a / g*b; };
ll MOD(ll x, ll m){return (x%m+m)%m; }
ll FLOOR(ll x, ll m) {ll r = (x%m+m)%m; return (x-r)/m; }
template<class T> using dijk = priority_queue<T, vector<T>, greater<T>>;
# define all(qpqpq)           (qpqpq).begin(),(qpqpq).end()
# define UNIQUE(wpwpw)        (wpwpw).erase(unique(all((wpwpw))),(wpwpw).end())
# define LOWER(epepe)         transform(all((epepe)),(epepe).begin(),TL<char>)
# define UPPER(rprpr)         transform(all((rprpr)),(rprpr).begin(),TU<char>)
# define rep(i,upupu)         for(ll i = 0, i##_len = (upupu);(i) < (i##_len);(i)++)
# define reps(i,opopo)        for(ll i = 1, i##_len = (opopo);(i) <= (i##_len);(i)++)
# define len(x)                ((ll)(x).size())
# define bit(n)               (1LL << (n))
# define pb push_back
# define eb emplace_back
# define exists(c, e)         ((c).find(e) != (c).end())

struct INIT{
	INIT(){
		std::ios::sync_with_stdio(false);
		std::cin.tie(0);
		cout << fixed << setprecision(20);
	}
}INIT;

namespace mmrz {
	void solve();
}

int main(){
	mmrz::solve();
}
#line 2 "graph/two_sat.hpp"

#line 2 "graph/strongly_connected_components.hpp"

#line 4 "graph/strongly_connected_components.hpp"

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;
	}
};
#line 5 "verify/yosupo/two_sat.test.cpp"

void mmrz::solve(){
	char _p;
	string _cnf;
	int n, m;
	cin >> _p >> _cnf >> n >> m;

	auto f = [](int x) -> pair<int, bool> {
		bool tf = (x > 0 ? true : false);
		x = abs(x)-1;
		return make_pair(x, tf);
	};

	two_sat ts(n);
	while(m--){
		int x, y, _zero;
		cin >> x >> y >> _zero;
		auto [nx, x_tf] = f(x);
		auto [ny, y_tf] = f(y);
		ts.add_clause(nx, x_tf, ny, y_tf);
	}

	auto ret = ts.solve();
	if(ret.empty()){
		cout << "s UNSATISFIABLE" << '\n';
		return;
	}
	cout << "s SATISFIABLE" << '\n';
	cout << "v";
	rep(i, n){
		cout << " " << (ret[i] ? "" : "-") << i+1;
	}
	cout << " 0" << '\n';
}
Back to top page