Submit Info #3043

Problem Lang User Status Time Memory
2 Sat cpp (anonymous) AC 818 ms 157.62 MiB

ケース詳細
Name Status Time Memory
cycle_unsat_00 AC 327 ms 153.64 MiB
cycle_unsat_01 AC 326 ms 157.62 MiB
example_00 AC 4 ms 0.62 MiB
example_01 AC 5 ms 0.62 MiB
max_random_00 AC 799 ms 100.41 MiB
max_random_01 AC 811 ms 100.39 MiB
max_random_02 AC 818 ms 100.40 MiB
max_random_03 AC 802 ms 100.46 MiB
max_random_04 AC 797 ms 100.36 MiB
random_00 AC 616 ms 77.73 MiB
random_01 AC 666 ms 90.65 MiB
random_02 AC 327 ms 23.30 MiB
random_03 AC 105 ms 55.98 MiB
random_04 AC 179 ms 44.62 MiB

#include <bits/stdc++.h> using namespace std; using ll = long long; using PII = pair<ll, ll>; #define FOR(i, a, n) for (ll i = (ll)a; i < (ll)n; ++i) #define REP(i, n) FOR(i, 0, n) #define ALL(x) x.begin(), x.end() template<typename T> void chmin(T &a, const T &b) { a = min(a, b); } template<typename T> void chmax(T &a, const T &b) { a = max(a, b); } struct FastIO {FastIO() { cin.tie(0); ios::sync_with_stdio(0); }}fastiofastio; #ifdef DEBUG_ #include "../program_contest_library/memo/dump.hpp" #else #define dump(...) #endif const ll INF = 1LL<<60; struct SCC { int V, K; vector<vector<int>> G; vector<vector<int>> rG; vector<int> vs; vector<int> used; vector<int> cmp; void dfs(int v) { used[v]=true; for(int nx: G[v]) if(!used[nx]) dfs(nx); vs.push_back(v); } void rdfs(int v,int k) { used[v]=true; cmp[v]=k; for(int nx: rG[v]) if(!used[nx]) rdfs(nx,k); } SCC() { V=K=-1; } SCC(int V_): V(V_), G(V_), rG(V_), used(V_), cmp(V_) {} void add_edge(int from,int to) { G[from].push_back(to); rG[to].push_back(from); } int scc() { used.assign(V,0); vs.clear(); for(int v=0;v<V;v++) if(!used[v]) dfs(v); used.assign(V,0); int k=0; for(int i=(int)vs.size()-1;i>=0;i--) if(!used[vs[i]]) { rdfs(vs[i],k++); } return K=k; } // O(ElogE) // SCCしたあとのグラフはトポロジカル順になってる vector<vector<int>> getDAG() { vector<vector<int>> res(K); for(int from=0;from<V;from++) { for(int to:G[from]) if(cmp[from]!=cmp[to]) { res[cmp[from]].push_back(cmp[to]); } } for(int i=0;i<K;i++){ sort(ALL(res[i])); res[i].erase(unique(ALL(res[i])),res[i].end()); } return res; } }; // (x_i1 and x_j1) or (x_i2 and x_j2) or … struct twoSAT { ll n; SCC graph; vector<bool> ans; twoSAT(ll n) : n(n), graph(n*2), ans(n) {} // not なら false void add(pair<ll,bool> a0, pair<ll,bool> b0) { ll a = a0.first, ar = (a0.first+n)%(2*n); ll b = b0.first, br = (b0.first+n)%(2*n); if(!a0.second) swap(a, ar); if(!b0.second) swap(b, br); graph.add_edge(ar, b); graph.add_edge(br, a); } bool solve() { graph.scc(); REP(i, n) if(graph.cmp[i] == graph.cmp[n+i]) return false; REP(i, n) ans[i] = graph.cmp[i] > graph.cmp[n+i]; return true; } }; int main () { ll n, m; string ss; cin >> ss >> ss >> n >> m; twoSAT graph(n); REP(i, m) { ll a, b, c; cin >> a >> b >> c; pair<ll, bool> p1, p2; if(a < 0) p1 = {-a-1, false}; else p1 = {a-1, true}; if(b < 0) p2 = {-b-1, false}; else p2 = {b-1, true}; graph.add(p1, p2); } if(!graph.solve()) { cout << "s UNSATISFIABLE" << endl; return 0; } cout << "s SATISFIABLE" << endl; cout << "v "; REP(i, n) cout << (graph.ans[i] ? 1 : -1) * (i+1) << " "; cout << "0" << endl; }