#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#include "template.hpp"
#include "graph/twosat.hpp"
int main(){
cin.tie(nullptr)->sync_with_stdio(false);
string s;
int n,m;
cin >> s >> s >> n >> m;
TwoSAT sat(n);
for(int i=0;i<m;i++){
int a,b,x;
cin >> a >> b >> x;
sat.add_clause(abs(a)-1,a<0,abs(b)-1,b<0);
}
auto [ok,ans]=sat.solve();
if(ok){
cout << "s SATISFIABLE\n";
cout << "v ";
for(int i=0;i<n;i++)cout << (ans[i]?i+1:-(i+1)) << " ";
cout << "0\n";
}else{
cout << "s UNSATISFIABLE\n";
}
}
#line 1 "verify/yosupo/graph/twosat/two_sat.test.cpp"
#define PROBLEM "https://judge.yosupo.jp/problem/two_sat"
#line 2 "template.hpp"
#include<bits/stdc++.h>
using namespace std;
using ll = long long;
using db = long double;
using i128 = __int128_t;
using u32 = uint32_t;
using u64 = uint64_t;
template<class T>
using PQ = priority_queue<T,vector<T>,greater<T>>;
const int INF=INT_MAX/2;
const ll LINF=LLONG_MAX/4;
const db DINF=numeric_limits<db>::infinity();
const db EPS=1e-9;
const db PI=acos(db(-1));
#define ALL(a) a.begin(),a.end()
#define RALL(a) a.rbegin(),a.rend()
#define SZ(a) (int)(a.size())
#define SORT(a) sort(ALL(a))
#define RSORT(a) sort(RALL(a))
#define REV(a) reverse(ALL(a))
#define UNI(a) a.erase(unique(ALL(a)),a.end())
#define LB(a,x) (int)(lower_bound(ALL(a),x)-a.begin())
#define UB(a,x) (int)(upper_bound(ALL(a),x)-a.begin())
#define FIND(a,x) (int)(find(ALL(a),x)-a.begin())
#define COUNT(a,x) (int)count(ALL(a),x)
#define MIN(a) *min_element(ALL(a))
#define MAX(a) *max_element(ALL(a))
template<class T,class U>
bool chmin(T &a,U b){return b<a?a=b,1:0;}
template<class T,class U>
bool chmax(T &a,U b){return a<b?a=b,1:0;}
template<class T>
T floor(T a,T b){return a/b-((a^b)<0&&a%b);}
template<class T>
T ceil(T a,T b){return a/b+((a^b)>=0&&a%b);}
int popcnt(ll x){return __builtin_popcountll(x);}
int topbit(ll x){return x==0?-1:63-__builtin_clzll(x);}
int lowbit(ll x){return x==0?-1:__builtin_ctzll(x);}
template<class T,class U>
T SUM(const U &a){return accumulate(ALL(a),T{});}
template<class T>
vector<int> argsort(const vector<T> &a){
vector<int> p(SZ(a));
iota(ALL(p),0);
stable_sort(ALL(p),[&](int i,int j){return a[i]<a[j];});
return p;
}
template<class T,size_t D=0>
struct VecBuilder{
array<size_t,D> d;
VecBuilder<T,D+1> operator[](size_t n)const{
VecBuilder<T,D+1> res{};
for(size_t i=0;i<D;i++)res.d[i]=d[i];
res.d[D]=n;
return res;
}
template<size_t I=0>
auto build(const T &x)const{
if constexpr(I+1==D)return vector<T>(d[I],x);
else return vector<decltype(build<I+1>(x))>(d[I],build<I+1>(x));
}
auto operator()(const T &x=T())const{
static_assert(D>0);
return build(x);
}
};
template<class T>
inline constexpr VecBuilder<T> VEC{};
mt19937 rng(chrono::steady_clock::now().time_since_epoch().count());
mt19937_64 rng64(chrono::steady_clock::now().time_since_epoch().count());
#line 3 "graph/twosat.hpp"
/**
* Author: Teetat T.
* Date: 2025-02-20
* Description: Cartesian Tree.
*/
struct TwoSAT{
int n;
vector<vector<int>> adj,rev;
TwoSAT(int _n):n(_n),adj(n*2),rev(n*2){}
void add_edge(int u,int v){
adj[u].emplace_back(v);
rev[v].emplace_back(u);
}
void add_clause(int u,bool nu,int v,bool nv){
u=(u<<1)|nu,v=(v<<1)|nv;
add_edge(u^1,v);
add_edge(v^1,u);
}
pair<bool,vector<bool>> solve(){
vector<bool> vis(n*2),ans(n);
vector<int> ord,scc(n*2);
int scc_id=0;
function<void(int)> dfs=[&](int u){
if(vis[u])return;
vis[u]=true;
for(auto v:adj[u])dfs(v);
ord.emplace_back(u);
};
function<void(int)> dfs2=[&](int u){
if(scc[u])return;
scc[u]=scc_id;
for(auto v:rev[u])dfs2(v);
};
for(int i=0;i<2*n;i++)dfs(i);
reverse(ord.begin(),ord.end());
for(int i:ord)if(!scc[i]){
scc_id++;
dfs2(i);
}
for(int i=0;i<n;i++){
if(scc[i<<1]==scc[(i<<1)|1])return {false,ans};
ans[i]=scc[i<<1]>scc[(i<<1)|1];
}
return {true,ans};
}
};
#line 4 "verify/yosupo/graph/twosat/two_sat.test.cpp"
int main(){
cin.tie(nullptr)->sync_with_stdio(false);
string s;
int n,m;
cin >> s >> s >> n >> m;
TwoSAT sat(n);
for(int i=0;i<m;i++){
int a,b,x;
cin >> a >> b >> x;
sat.add_clause(abs(a)-1,a<0,abs(b)-1,b<0);
}
auto [ok,ans]=sat.solve();
if(ok){
cout << "s SATISFIABLE\n";
cout << "v ";
for(int i=0;i<n;i++)cout << (ans[i]?i+1:-(i+1)) << " ";
cout << "0\n";
}else{
cout << "s UNSATISFIABLE\n";
}
}
verify/yosupo/graph/twosat/two_sat.test.cpp