2-SAT两篇论文《由对称性解2-SAT问题》（伍昱的WC论文）、《2-SAT解法浅析》（赵爽）我就不多说了，伍昱的论文以实例说明了2-SAT的建图方式，赵爽的论文则比较偏重理论。首先关于建图，如果两点a和b矛盾则a和非b连一条边，而不能是如果选a后可以选b则连边ab，看起来没好像什么区别但是实际上会引起错误，我一开始写2-SAT时就因为这一点一直写错，后来才把这点弄清。
关于输出答案的部分，拓扑排序然后建反向图什么的，其实我一直在想为什么不是建正向图，好像是因为必要条件什么的，没有想得很清楚，以后想清楚了再来补上。
POJ 2723
这个题是刚才写完的，题意：
有2*n把钥匙分成n组，每组两个钥匙如果选择了一把另一把就会消失。有m个门，每个门上有两把锁，只要打开一把锁就能打开门，要打开第i+1个门必须先打开第i个门。问最多能打开多少门。
首先考虑到如果能打开x+1个门那必然能打开i个门，那么可以二分答案。接下来是验证。
2-SAT建图方式如下：
每把钥匙拆成两个点，分别代表选和不选；
对于每个组的两把钥匙i和j，如果选了i就不能选j，同理，选了j就不能选i，那么对于每一组两把钥匙连两条边<i,非j>和<j,非i>；
对于每个门上的两个锁u和v，不选u则一定要选v， 不选v一定要选u，于是对于每个门，连两条边<i非,j>和<非j,i>，
注意到如果门上的两把锁是相同的则这把钥匙必选，那么连边<非i,i>。
POJ 2749
这个题的题意好像是平面上有两个点s1和s2，这两个点是连在一起的，然后给了n个点，然后这些点要么连s1要么连s2，要求任意两点的最大距离最小，然后有些点不能连在同一边，也就是不能同时连s1或者s2，有些点必须连在同一边，就是同时连s1或者同时连s2。这题要求的是曼哈顿距离。两个点a和b的距离有4种，a->s1->b ; a->s2->b ; a->s1->s2->b ; a->s2->s1->b。
首先一看到最大最小一定是二分答案。然后2-SAT模型也比较明显，每个点拆成两个点分别表示连s1和连s2。
我就是在这个题的建图上犯了上面说的ab不矛盾则连边ab的错误，一整节DSP课都在想建图模型然后画了4、5个都推翻了。
建图方式首先是把要求的不能连同一边的和必须连同一边的点连好边，然后枚举每一对点，分四种情况建边，这里直接上代码可能会比较明白：
for(i=0;i<n;i++)
for(j=i+1;j<n;j++)
{
if(fd[i]+fd[j]>mid)
{
addedge(i*2,j*2+1);
addedge(j*2,i*2+1);
}
if(fd[i]+dss+fe[j]>mid)
{
addedge(i*2,j*2);
addedge(j*2+1,i*2+1);
}
if(fe[i]+dss+fd[j]>mid)
{
addedge(i*2+1,j*2+1);
addedge(j*2,i*2);
}
if(fe[i]+fe[j]>mid)
{
addedge(i*2+1,j*2);
addedge(j*2+1,i*2);
}
}
这里fd[i]和fe[i]分别代表点i与s1 s2的距离，dss是s1和s2之间的距离。然后就是2-sat验证了。
POJ 3207
写这个题的时候我还没有准备自己的2-SAT模板，还是抄别人的。现在觉得还是自己写的代码看着舒服。
题意：一个圆周上有n个点标号依次从0到n-1，然后有m条线段每个线段以其中两个点为端点，线可以在圆正面或者背面，问是否存在一种方式使得任意两线段都不相交，端点相交不算。
每条线要么在正面要么在背面，以此建立2-sat模型，于是问题就在于如何判断两个线段是否相交，对于两个线段x0,y0和x1,y1，保证x0<y0 && x1<y1，满足如下条件则会相交，此时两线不能在同一面：
(x0-x1)*(x0-y1)*(y0-x1)*(y0-y1) < 0
POJ 3648
这个题是一个要输出方案的2-sat。
题意：一堆夫妇去参加一对新人的婚礼。人们坐在一个很长很长的桌子的两侧（面对面）。新郎新娘在桌子头面对面座。
新娘不希望看见她对面的一排有一对夫妇坐着（夫妇需要分开两排座）。
同时，一些人之间有暧昧关系（同性异性均有可能），新娘也不希望有暧昧关系的人同时坐在她对面的一排。
问你可否满足新娘的要求，可以的话，输出一种方案。
囧~这题题意不好说直接复制别人的了。
每对夫妻只有一个能坐在新娘一边，可以以每对夫妻为一组点，有暧昧关系的两个人不能同时坐在新娘对面，以此为矛盾关系建图。然后新郎和新娘不能坐在同一边，所以要连一条边从新郎指向新娘。
这个题是要输出方案的，这部分也同样是模板，论文里有说明，这里不多说。
POJ 3678
题意：构造一个长度为N的01数列，使得第i位和第j位通过特定的逻辑运算结果为k。
每组点分别代表0和1，按逻辑运算建边，水题一个。
看到这个题我就想去长春赛的B题，如果长春赛前做了这个题那现场一定能快速想到那题用2-sat写而不是按位生成暴力验证，于是就不会WA两个小时了TAT。
POJ 3683
题意：一个牧师要主持N场婚礼，主持时长为x，中间不能间断，可以选择在婚礼开始时主持或者婚礼结束时主持，也就是开始到开始时间+x或者结束时间-x到结束时间。一场婚礼结束后可以立刻另一场婚礼。
按主持开始和结束时间之间是否重叠建图，这题建图写起来好烦，两个婚礼一共四种重叠方式，然后做这个题时我又把建图想错了，又想的是不矛盾直接连边，结果WA了一片。另外这题也是要输出方案。
POJ上一共有8道2-SAT，还有两个分别是POJ2296和POJ3905，这两个题我还没有写TAT
附2-SAT模板
//POJ 3683
#include <cstdio>
#include <cstring>
#include <cstdlib>
#include <cmath>
#include <iostream>
#include <string>
#include <algorithm>
#include <queue>
#include <map>
#include <stack>
using namespace std;
#define PI acos(-1)
#define INF 1<<30
#define EPS 1e-6
#define SET(a,b) memset(a,b,sizeof(a))
#define N 2010
#define M 4000010
int n,m;
int head[N],next[M],e[M],cnt;
int nhead[N],nnext[M],ne[M],ncnt;
int shead[N],snext[M],se[M],scnt;
int dfn[N],low[N],step,point,ins[N];
stack<int> st;
int into[N],color[N],color2[N];
int tl[N][2],tr[N][2],sp[N];
int ts[N],tt[N];
void addedge(int *head,int *next,int *e,int &cnt,int u,int v)
{
next[cnt]=head[u];
e[cnt]=v;
head[u]=cnt++;
}
void tarjan(int u)
{
int i,j,v;
dfn[u]=low[u]=++step;
st.push(u);
ins[u]=1;
for(i=head[u];i!=-1;i=next[i])
{
v=e[i];
if(! dfn[v])
{
tarjan(v);
low[u]=min(low[u],low[v]);
}else
if(ins[v]) low[u]=min(low[u],dfn[v]);
}
if(dfn[u]==low[u])
{
do{
j=st.top();
st.pop();
color[j]=point;
ins[j]=0;
} while (j!=u);
point++;
}
}
bool twosat(int n)
{
for(int i=0;i+1<n;i+=2)
if(color[i]==color[i+1]) return 0;
return 1;
}
void COLOR(int s)
{
color2[s]=1;
for(int i=nhead[s];i!=-1;i=nnext[i])
if(color2[ne[i]]==-1) COLOR(ne[i]);
}
void findans(int n)
{
memset(into,0,sizeof(into));
memset(color2,-1,sizeof(color2));
memset(shead,-1,sizeof(shead));
scnt=0;
for(int i=0;i<n;i++)
addedge(shead,snext,se,scnt,color[i],i);
ncnt=0;
memset(nhead,-1,sizeof(nhead));
for(int i=0;i<n;i++)
for(int j=head[i];j!=-1;j=next[j])
if(color[i]!=color[e[j]])
{
addedge(nhead,nnext,ne,ncnt,color[e[j]],color[i]);
into[color[i]]++;
}
queue<int> Q;
for(int i=0;i<point;i++)
if(into[i]==0) Q.push(i);
while (! Q.empty())
{
int x=Q.front();
Q.pop();
if(color2[x]!=-1) continue;
color2[x]=0;
for(int i=nhead[x];i!=-1;i=nnext[i])
{
into[ne[i]]--;
if(into[ne[i]]==0) Q.push(ne[i]);
}
for(int i=shead[x];i!=-1;i=snext[i])
if(color2[color[se[i]^1]]==-1) COLOR(color[se[i]^1]);
}
memset(color,0,sizeof(color));
for(int i=0;i<point;i++)
if(color2[i]==1)
for(int j=shead[i];j!=-1;j=snext[j]) color[se[j]]=1;
for(int i=0;i<n;i++)
if(color[i]==0)
{
if(i%2==0)
{
printf("%02d:%02d ",tl[i/2][0],tl[i/2][1]);
printf("%02d:%02d\n",(ts[i/2]+sp[i/2])/60,(ts[i/2]+sp[i/2])%60);
}
else
{
printf("%02d:%02d",(tt[i/2]-sp[i/2])/60,(tt[i/2]-sp[i/2])%60);
printf(" %02d:%02d\n",tr[i/2][0],tr[i/2][1]);
}
}
}
int main ()
{
while(scanf("%d",&n)!=-1)
{
for(int i=0;i<n;i++)
{
scanf("%d:%d %d:%d %d",&tl[i][0],&tl[i][1],&tr[i][0],&tr[i][1],&sp[i]);
ts[i]=tl[i][0]*60+tl[i][1];
tt[i]=tr[i][0]*60+tr[i][1];
}
memset(head,-1,sizeof(head));
cnt=0;
for(int i=0;i<n;i++)
for(int j=0;j<n;j++)
if(i!=j)
{
if(ts[i]<=ts[j] && ts[i]+sp[i]>ts[j] || ts[i]<ts[j]+sp[j] && ts[i]+sp[i]>=ts[j]+sp[j])
{
addedge(head,next,e,cnt,i*2,j*2+1);
addedge(head,next,e,cnt,j*2,i*2+1);
}
if(ts[i]<tt[j] && ts[i]+sp[i]>=tt[j] || ts[i]<=tt[j]-sp[j] && ts[i]+sp[i]>tt[j]-sp[j])
{
addedge(head,next,e,cnt,i*2,j*2);
addedge(head,next,e,cnt,j*2+1,i*2+1);
}
if(tt[i]-sp[i]<=ts[j] && tt[i]>ts[j] || tt[i]-sp[i]<ts[j]+sp[j] && tt[i]>=ts[j]+sp[j])
{
addedge(head,next,e,cnt,i*2+1,j*2+1);
addedge(head,next,e,cnt,j*2,i*2);
}
if(tt[i]-sp[i]<tt[j] && tt[i]>=tt[j] || tt[i]-sp[i]<=tt[j]-sp[j] && tt[i]>tt[j]-sp[j])
{
addedge(head,next,e,cnt,i*2+1,j*2);
addedge(head,next,e,cnt,j*2+1,i*2);
}
}
/*for(int i=0;i<n*2;i++)
for(int j=head[i];j!=-1;j=next[j])
printf("%d %d\n",i,e[j]);*/
point=step=0;
memset(dfn,0,sizeof(dfn));
for(int i=0;i<n*2;i++)
if(! dfn[i]) tarjan(i);
//for(int i=0;i<n*2;i++) printf("%d ",color[i]); printf("\n");
if(! twosat(n*2)) printf("NO\n");
else
{
printf("YES\n");
findans(2*n);
}
}
return 0;
}