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\n");
139 printf("%d",cont);
140 for(int i=0;i<cont;i++)
141 {
142 printf(" %d",output[i]);
143 }
144 printf("\n");
145 }
146 else printf("No\n");
147 }
148 }