定义
SAT是适定性(Satisfiability)问题的简称 。一般形式为k-适定性问题，简称 k-SAT。
可以证明，当 \(k>2\) 时，k-SAT 是 NP 完全的。因此一般讨论的是 \(k=2\) 的情况，即 2-SAT 问题。
我们通俗的说，有 \(n\) 个布尔变量 \(x_{1}−x_{n}\)。给出 \(m\) 个限制关系，每个关系最多只对两个变量进行限制。求一组取值使得满足所有限制。
这里的限制例如：选 \(A\)必选 \(B\) 或是 \(A\)，\(B\) 至少选一个。
也就是“ \(x_{i}=0\) 或（“或”也可能是“与”“异或”等） \(x_{j}=1\) ”形似这类的条件。
而求解 2-SAT 的解就是求出满足所有限制的一组答案。
建图
我们把 \(x_{1}-x_{n}\) 这 \(n\) 个点给拆成 \(2n\) 个点，点 \(x_{i}\) 表示 \(x_{i}\) 的值为 \(1\)，点 \(x_{i+n}\) 表示 \(x_{i}\) 的值为 \(0\)。
假如说我们有一个限制条件：“\(x_{i}\) & \(x_{j}=0\) ”
那么这说明 \(x_{i}\) 和 \(x_{j}\) 之中至少有一个为 \(0\)
这时我们从 \(x_{i}\) 向 \(x_{j+n}\) 连边，从 \(x_{j}\) 向 \(x_{i+n}\) 连边。
只有在关系明确的时候才能建边
拿上面的限制来说，如果当 \(x_{i}\) 为 \(1\) 的时候，那么 \(x_{j}\) 为 \(0\) 的时候才能满足关系，同理当 \(x_{j}\) 为 \(1\) 的时候，只有 \(x_{i}\) 为 \(0\) 的时候才满足限制。
为什么不从 \(x_{j+n}\) 向 \(x_{i}\) 或者 \(x_{i+n}\) 到 \(x_{j}\) 连边呢？
因为当其中一个值为 \(0\) 的时候，另一个的值为 \(0\) 或 \(1\) 都是满足条件的。
若 “ \(x_{a}=p\) 或 \(x_{b}=q\) ” 中至少有一个满足，那么我们建两条有向边：
可以简单总结为：其中一个不成立则另一个一定成立（这是明确的关系）
如果出现类似 \(x_{i}=1\) 这种关系的话，我们就从 \(x_{i+n}\) 向 \(x_{i}\) 连边，表示从当前 \(x_{i}\) 等于 \(0\) 的点也是走到 \(x_{i}\) 为 \(1\) 的点。
求解
我们通常是跑一遍 tarjan 求强连通分量，如果要是有一个点 \(x_{i}\) 和 \(x_{i+n}\) 在同一个强连通分量说明无解，因为此时的情况 \(x_{i}\) 没有取值可以满足所有的关系，说明此时限制互相矛盾。
P4782 【模板】2-SAT 问题
code：
#include<bits/stdc++.h>
#define int long long
#define N 4000100
using namespace std;
int head[N],cnt,n,m,f[N],dep[N],tp[N],tot;
struct sb{int u,v,next;}e[N];
inline int read(){int x=0,f=1;char ch=getchar();while(!isdigit(ch)){f=ch!='-';ch=getchar();}while(isdigit(ch)){x=(x<<1)+(x<<3)+(ch^48);ch=getchar();}return f?x:-x;}
inline void add(int u,int v){e[++cnt].u=u;e[cnt].v=v;e[cnt].next=head[u];head[u]=cnt;}
inline int fid(int x){if(f[x]==x)return x;return f[x]=fid(f[x]);}
inline void dfs(int x)
{
for(int i=head[x];i;i=e[i].next)
{
int v=e[i].v;
if(!dep[v])dep[v]=dep[x]+1,dfs(v);
if(dep[fid(v)]>0)
{
if(dep[fid(x)]<dep[f[v]])f[f[v]]=f[x];
else f[f[x]]=f[v];
}
}
dep[x]=-1,tp[x]=++cnt;
}
signed main()
{
n=read();m=read();
for(int i=1;i<=2*n;i++)f[i]=i;
for(int i=1;i<=m;i++)
{
int a=read(),b=read(),c=read(),d=read();
add(a+n*(b&1),c+n*(d^1));
add(c+n*(d&1),a+n*(b^1));
}
for(int i=1;i<=2*n;i++)if(!dep[i])dfs(i);
for(int i=1;i<=n;i++)if(fid(i)==fid(i+n))return cout<<"IMPOSSIBLE"<<endl,0;
cout<<"POSSIBLE"<<endl;
for(int i=1;i<=n;i++)
{
int ii=i+n;
if(tp[fid(i)]<tp[fid(ii)])cout<<"1 "<<endl;
else cout<<"0 "<<endl;
}
return 0;
}
tarjan 版：
#include<bits/stdc++.h>
#define N 4000100
using namespace std;
int n,m,ti,ans,head[N],nxt[N],to[N],dfn[N],low[N];
int flag[N],vis[N],cnt,sd[N],stk[N],top;
inline void add(int u,int v){to[++cnt]=v;nxt[cnt]=head[u];head[u]=cnt;}
void tarjan(int x)
{
cnt=0;
dfn[x]=low[x]=++ti;
vis[x]=flag[x]=1;stk[++top]=x;
for(int i=head[x];i;i=nxt[i])
{
int v=to[i];
if(!dfn[v])tarjan(v),low[x]=min(low[x],low[v]);
else if(vis[v])low[x]=min(low[x],dfn[v]);
}
if(dfn[x]==low[x])
{
int y;cnt++;
while(1)
{
y=stk[top--];
sd[y]=cnt;
vis[y]=0;
if(x==y)break;
}
}
}
signed main()
{
cin>>n>>m;
for(int i=1;i<=m;i++)
{
int a,b,c,d;
cin>>a>>b>>c>>d;
add(a+n*b,c+n*(1^d));
add(c+n*d,a+n*(1^b));
}
for(int i=1;i<=2*n;i++)
if(!flag[i])tarjan(i);
// for(int i=1;i<=2*n;i++)
// cout<<sd[i]<<' ';
// cout<<endl;
for(int i=1;i<=n;i++)
if(sd[i]==sd[i+n]){cout<<"IMPOSSIBLE"<<endl;return 0;}
cout<<"POSSIBLE"<<endl;
for(int i=1;i<=n;i++)
cout<<(sd[i]<sd[i+n])<<" ";
return 0;
}