2-Sat+输出可行解：
1 //LightOJ 1251 2 #include<stdio.h> 3 #include<string.h> 4 #include<vector> 5 #include<queue> 6 using namespace std; 7 int output[40005]; 8 int vis[70005]; 9 int low[70005]; 10 int dfn[70005]; 11 int print[70005]; 12 int stack[70005]; 13 int color[70005]; 14 int pos[70005]; 15 int degree[70005]; 16 vector<int >mp[70005]; 17 vector<int >mp2[70005]; 18 int n,m,sig,cnt,tot,cont; 19 void add(int x,int y) 20 { 21 mp[x].push_back(y); 22 } 23 void top() 24 { 25 memset(print,0,sizeof(print)); 26 queue<int >s; 27 for(int i=1;i<=sig;i++) 28 { 29 if(degree[i]==0) 30 { 31 s.push(i); 32 } 33 } 34 while(!s.empty()) 35 { 36 int u=s.front(); 37 if(print[u]==0) 38 { 39 print[u]=1;print[pos[u]]=2; 40 } 41 s.pop(); 42 for(int i=0;i<mp2[u].size();i++) 43 { 44 int v=mp2[u][i]; 45 degree[v]--; 46 if(degree[v]==0)s.push(v); 47 } 48 } 49 cont=0; 50 for(int i=1;i<=n;i++)if(print[color[i]]==1)output[cont++]=i; 51 } 52 void Tarjan(int u) 53 { 54 vis[u]=1; 55 dfn[u]=low[u]=cnt++; 56 stack[++tot]=u; 57 for(int i=0;i<mp[u].size();i++) 58 { 59 int v=mp[u][i]; 60 if(vis[v]==0)Tarjan(v); 61 if(vis[v]==1)low[u]=min(low[u],low[v]); 62 } 63 if(low[u]==dfn[u]) 64 { 65 sig++; 66 do 67 { 68 vis[stack[tot]]=-1; 69 color[stack[tot]]=sig; 70 } 71 while(stack[tot--]!=u); 72 } 73 } 74 int Slove() 75 { 76 sig=0; 77 cnt=1; 78 tot=-1; 79 memset(degree,0,sizeof(degree)); 80 memset(stack,0,sizeof(stack)); 81 memset(dfn,0,sizeof(dfn)); 82 memset(low,0,sizeof(low)); 83 memset(vis,0,sizeof(vis)); 84 memset(color,0,sizeof(color)); 85 for(int i=1;i<=n*2;i++) 86 { 87 if(vis[i]==0) 88 { 89 Tarjan(i); 90 } 91 } 92 for(int i=1;i<=n;i++) 93 { 94 if(color[i]==color[i+n])return 0; 95 pos[color[i]]=color[i+n]; 96 pos[color[i+n]]=color[i]; 97 } 98 for(int i=1;i<=n*2;i++) 99 { 100 for(int j=0;j<mp[i].size();j++) 101 { 102 int v=mp[i][j]; 103 if(color[i]!=color[v]) 104 { 105 degree[color[i]]++; 106 mp2[color[v]].push_back(color[i]); 107 } 108 } 109 } 110 top(); 111 return 1; 112 } 113 int main() 114 { 115 int t; 116 int kase=0; 117 scanf("%d",&t); 118 while(t--) 119 { 120 scanf("%d%d",&m,&n); 121 for(int i=1;i<=60000;i++)mp[i].clear(),mp2[i].clear(); 122 for(int i=0;i<m;i++) 123 { 124 int x,y; 125 scanf("%d%d",&x,&y); 126 int xx=x;int yy=y; 127 if(x<0)x=-x; 128 if(y<0)y=-y; 129 if(xx>0&&yy>0)add(x+n,y),add(y+n,x); 130 if(xx>0&&yy<0)add(x+n,y+n),add(y,x); 131 if(xx<0&&yy>0)add(x,y),add(y+n,x+n); 132 if(xx<0&&yy<0)add(x,y+n),add(y,x+n); 133 } 134 int ans=Slove(); 135 printf("Case %d: ",++kase); 136 if(ans==1) 137 { 138 printf("Yes "); 139 printf("%d",cont); 140 for(int i=0;i<cont;i++) 141 { 142 printf(" %d",output[i]); 143 } 144 printf(" "); 145 } 146 else printf("No "); 147 } 148 }