最近看了人工智能的确定性推理，对2-SAT有了更深的理解，感觉2-SAT构图过程就是构建的一个推理图，逻辑关系是a->b。根据这题实际来讲讲
就用第一种情况来举例吧
A被选或者B被选或者两者都发生都是可以被接受的。
那么如果A没有被选，我们能推出B被选了。同样如果B没有被选，我们能推出A被选了，其他我们不能推出任何结论。
所以构造关系
!B->A
!A->B
反应到图上就是两条边。
这样构图完成后找出图里所有的强连通分量，如果A和!A在同一个强连通分量里，那么就冲突了。（我们能推理出A->!A）
代码：
1 Source Code 2
3 Problem: 3905 User: yzhw
4 Memory: 16168K Time: 2297MS
5 Language: GCC Result: Accepted
6 Source Code
7 # include <stdio.h>
8 # include <stdlib.h>
9 # include <string.h>
10 # define N 2000
11 # define M 1000000*2
12 # define min(a,b) ((a)<(b)?(a):(b))
13 # define abs(a) ((a)>0?(a):-(a))
14 int n,m;
15 int p,nxt[M],g[N],v[M];
16 int stack[N],sp,dfn,low[N];
17 void insert(int a,int b)
18 {
19 v[p]=b;
20 nxt[p]=g[a];
21 g[a]=p++;
22 }
23 int dfs(int pos)
24 {
25 int minnum=dfn++;
26 int p;
27 stack[sp++]=pos;
28 low[pos]=minnum;
29 for(p=g[pos];p!=-1;p=nxt[p])
30 {
31 if(low[v[p]]==-1)
32 if(!dfs(v[p])) return 0;
33 minnum=min(minnum,low[v[p]]);
34 }
35 if(minnum<low[pos]) low[pos]=minnum;
36 else
37 {
38 do
39 {
40 low[stack[sp-1]]=N;
41 if(abs(stack[sp-1]-pos)==n) return 0;
42 sp--;
43 }while(stack[sp]!=pos);
44 }
45 return 1;
46 }
47 int main()
48 {
49 while(scanf("%d%d",&n,&m)!=EOF)
50 {
51 int i,flag=1;
52 memset(g,-1,sizeof(g));
53 p=0;
54 for(i=0;i<m;i++)
55 {
56 char str1[32],str2[32];
57 int num1,num2;
58 scanf("%s%s",str1,str2);
59 num1=atoi(str1+1)-1;
60 num2=atoi(str2+1)-1;
61 if(*str1=='+'&&*str2=='+')
62 {
63 insert(num1+n,num2);
64 insert(num2+n,num1);
65 }
66 else if(*str1=='-'&&*str2=='-')
67 {
68 insert(num1,num2+n);
69 insert(num2,num1+n);
70 }
71 else if(*str1=='+'&&*str2=='-')
72 {
73 insert(num1+n,num2+n);
74 insert(num2,num1);
75 }
76 else
77 {
78 insert(num1,num2);
79 insert(num2+n,num1+n);
80 }
81 }
82 memset(low,-1,sizeof(low));
83 dfn=sp=0;
84 for(i=0;i<2*n&&flag;i++)
85 if(low[i]==-1)
86 if(!dfs(i)) flag=0;
87 printf("%d\n",flag);
88 }
89 return 0;
90 }