$2-SAT$用于求解以下问题是否有可行解：
有$n$个布尔变量$x_1…x_n$和$m$个需要满足的条件，每个条件形式为：$x_i=0(1) \ or \ x_j=0(1)$。
注意到以上条件等价于不选$A$条件，就必须要选$B$条件；不选$B$条件，就必须要选$A$条件。
那么不妨在（非$A$条件，$B$条件）和（非$B$条件，$A$条件）之间连边，即在$A$能推理出$B$的条件下连一条$A$到$B$的边。
如果$A$条件和非$A$条件在同一个强连通分量里面，证明$A$条件能推理出非$A$条件，这自相矛盾，无解。
注意使用两倍空间存储反向边，模板题：
// tarjan
void tarjan(int u)
{
dfn[u]=low[u]=++timer;
s.push(u);
vis[u]=1;
for(auto v:e[u])
{
if(!dfn[v])
tarjan(v),
low[u]=min(low[u],low[v]);
else if(vis[v])
low[u]=min(low[u],dfn[v]);
}
if(low[u]==dfn[u])
{
int v;
color++;
do
{
v=s.top();
s.pop();
vis[v]=0;
co[v]=color;
}
while(u!=v);
}
}
// 2-SAT的solve函数
bool solve()
{
for(int i=1;i<=2*n;++i)
if(!dfn[i]) tarjan(i);
for(int i=1;i<=n;++i)
if(co[i]==co[i+n])
return 0;
return 1;
}
// 建反向边
void add(int x,int y)
{
e[x].push_back(y);
}
for(int i=1;i<=m;++i)
{
scanf("%d%d%d%d",&a,&va,&b,&vb);
int nota=va^1,notb=vb^1;
add(a+nota*n,b+vb*n);//not a and b
add(b+notb*n,a+va*n);//not b and a
}
// 输出答案
if(solve())
{
puts("POSSIBLE");
for(int i=1;i<=n;++i)
printf("%d ",co[i]>co[i+n]);
}
else puts("IMPOSSIBLE");
完整代码参见：代码。