2-SAT 模板

在实际问题中，2-SAT问题在大多数时候表现成以下形式：有N对物品，每对物品中必须选取一个，也只能选取一个，并且它们之间存在某些限制关系（如某两个物品不能都选，某两个物品不能都不选，某两个物品必须且只能选一个，某个物品必选）等，这时，可以将每对物品当成一个布尔值（选取第一个物品相当于0，选取第二个相当于1），如果所有的限制关系最多只对两个物品进行限制，则它们都可以转化成9种基本限制关系，从而转化为2-SAT模型。

【建模】

其实2-SAT问题的建模是和实际问题非常相似的。

建立一个2N阶的有向图，其中的点分为N对，每对点表示布尔序列A的一个元素的0、1取值（以下将代表A[i]的0取值的点称为i，代表A[i]的1取值的点称为i'）。显然每对点必须且只能选取一个。然后，图中的边具有特定含义。若图中存在边<i, j>，则表示若选了i必须选j。可以发现，上面的9种限制关系中，后7种二元限制关系都可以用连边实现，比如NOT(A[x] AND A[y])需要连两条边<x, y'>和<y, x'>，A[x] OR A[y]需要连两条边<x', y>和<y', x>。而前两种一元关系，对于A[x]（即x必选），可以通过连边<x',
x>来实现，而NOT A[x]（即x不能选），可以通过连边<x, x'>来实现。

#include<stdio.h>
#include<algorithm>
#include<string.h>
#include<iostream>
#include<math.h>
using namespace std;
const int MAXN=210;
const int MAXM=40005;//边的最大数
struct Edge
{
int to,next;
}edge1[MAXM],edge2[MAXM];
int head1[MAXN];
int head2[MAXN];
int tol1,tol2;
bool vis1[MAXN],vis2[MAXN];
int Belong[MAXN];//连通分量标记
int T[MAXN];//dfs结点结束时间
int Bcnt,Tcnt;

//事件a^1代表a不成立，相邻存储
void add(int a,int b)//添加条件：若a成立则b成立
{
edge1[tol1].to=b;
edge1[tol1].next=head1[a];
head1[a]=tol1++;
edge2[tol2].to=a;
edge2[tol2].next=head2[b];
head2[b]=tol2++;
}
void init()//建图前初始化
{
memset(head1,-1,sizeof(head1));
memset(head2,-1,sizeof(head2));
memset(vis1,false,sizeof(vis1));
memset(vis2,false,sizeof(vis2));
tol1=tol2=0;
Bcnt=Tcnt=0;
}
void dfs1(int x)//对原图进行dfs,算出每个结点的结束时间，哪个点开始无所谓
{
vis1[x]=true;
int j;
for(int j=head1[x];j!=-1;j=edge1[j].next)
if(!vis1[edge1[j].to])
dfs1(edge1[j].to);
T[Tcnt++]=x;
}
void dfs2(int x)
{
vis2[x]=true;
Belong[x]=Bcnt;
int j;
for(j=head2[x];j!=-1;j=edge2[j].next)
if(!vis2[edge2[j].to])
dfs2(edge2[j].to);
}
bool ok(int n)//判断可行性
{
for(int i=0;i<2*n;i++)
if(!vis1[i])
dfs1(i);
for(int i=Tcnt-1;i>=0;i--)
if(!vis2[T[i]])//这个别写错，是vis2[T[i]]
{
dfs2(T[i]);
Bcnt++;
}
for(int i=0;i<=2*n-2;i+=2)
if(Belong[i]==Belong[i+1])
return false;
return true;
}