最近看了人工智能的確定性推理，對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 }