1. 拆点 : 将每个 bool 变量拆成 0, 1 两个点.

2. 连边 : 将限制条件转化为连边.

3. 图是 DAG 时, 对于每个 bool 变量, 合法点的拓扑序大于非法点.

   证明 : 若某个 bool 变量拆分成的两个点为 u,v , 若 u 为非法点, 则存在一条从 u 到 v 的路径, 所以 v 的拓扑序一定大于 u 的拓扑序.

4. 当图不是 DAG 时, 用 Tarjan 算法将强联通分量缩成一个点, 把原图变为 DAG.

5. Tarjan 求完强联通分量后不用缩点, 判断两个点所属的强联通分量序号即可, 序号小的为合法点.

证明 : 根据 Tarjan 求强联通分量的过程可知, 若存在一条从点 u 到点 v 的路径, 则 v 所属的强联通分量一定会在 u 所属的强联通分量之前被统计到, 所以点 v 所属的强联通分量序号更小.

6. 当一个 bool 变量拆分成的两个点在同一个强联通分量里, 则无解.

7. 若拆分成的两个点直接没有路径相连, 则随意选一个点即可.

【模板】2-SAT 问题

#include<bits/stdc++.h>
using namespace std;
const int _=2e6+7;
int n,m,dfn[_],low[_],bel[_],stk[_],top,cnt,num;
int lst[_],nxt[_],to[_],tot;
bool ins[_];

void add(int x,int y){
    nxt[++tot]=lst[x]; to[tot]=y; lst[x]=tot;
}

void _init(){
    cin>>n>>m;
    int x,u,y,v;
    for(int i=1;i<=m;i++){
	cin>>x>>u>>y>>v;
	add(x+(!u)*n,y+v*n);
	add(y+(!v)*n,x+u*n);
    }
}

void _dfs(int u){
    dfn[u]=low[u]=++cnt;
    stk[++top]=u; ins[u]=1;
    for(int i=lst[u];i;i=nxt[i]){
	int v=to[i];
	if(dfn[v]&&ins[v]) low[u]=min(low[u],dfn[v]);
	else if(!dfn[v]) _dfs(v),low[u]=min(low[u],low[v]);
    }
    if(low[u]==dfn[u]){
	num++;
	while(stk[top]!=u) bel[stk[top]]=num,ins[stk[top--]]=0;
	bel[u]=num,ins[u]=0;
	top--;
    }
}	    

void _run(){
    for(int i=1;i<=n+n;i++){
	if(!dfn[i]) _dfs(i);
	if(bel[i]==bel[i>n ?i-n :i+n]){ puts("IMPOSSIBLE"); return; }
    }
    puts("POSSIBLE");
    for(int i=1;i<=n;i++)
	printf("%d ",bel[i]>bel[i+n]);
    putchar('\n');
}

int main(){
#ifndef ONLINE_JUDGE

    freopen("x.in","r",stdin);
#endif
    ios::sync_with_stdio(false);
    _init();
    _run();
    return 0;
}